refactor: default binRoot to Main and expand init code

Lake/Init.lean

@@ -17,12 +17,20 @@ def toolchainFileName : FilePath :=
 def gitignoreContents :=
 s!"/{defaultBuildDir}\n/{defaultDepsDir}\n"
 
-def mainFileName (pkgName : String) : FilePath :=
-  s!"{pkgName.capitalize}.lean"
+def libFileName (libName : String) : FilePath :=
+  s!"{libName}.lean"
 
-def mainFileContents :=
-"def main : IO Unit :=
-  IO.println \"Hello, world!\"
+def libFileContents :=
+  s!"def hello := \"world\""
+
+def mainFileName : FilePath :=
+  s!"{defaultBinRoot}.lean"
+
+def mainFileContents (libName : String) :=
+s!"import {libName.toName.toString}
+
+def main : IO Unit :=
+  IO.println s!\"Hello, \{hello}!\"
 "
 
 def pkgConfigFileContents (pkgName : String) :=
@@ -44,10 +52,14 @@ def initPkg (dir : FilePath) (name : String) : IO PUnit := do
     throw <| IO.userError "package already initialized"
   IO.FS.writeFile configFile (pkgConfigFileContents name)
 
-  -- write example main module if none exists
-  let mainFile := dir / mainFileName name
+  -- write example code if the files do not already exist
+  let libName := name.capitalize
+  let libFile := dir / libFileName libName
+  unless (← libFile.pathExists) do
+    IO.FS.writeFile libFile libFileContents
+  let mainFile := dir / mainFileName
   unless (← mainFile.pathExists) do
-    IO.FS.writeFile mainFile mainFileContents
+    IO.FS.writeFile mainFile <| mainFileContents libName
 
   -- write current toolchain to file for `elan`
   IO.FS.writeFile (dir / toolchainFileName) <| leanVersionString ++ "\n"

Lake/Package.lean

@@ -37,6 +37,9 @@ def defaultIrDir : FilePath := "ir"
 /-- The default setting for a `PackageConfig`'s `depsDir` option. -/
 def defaultDepsDir : FilePath := "lean_packages"
 
+/-- The default setting for a `PackageConfig`'s `binRoot` option. -/
+def defaultBinRoot : Name := `Main
+
 --------------------------------------------------------------------------------
 -- # PackageConfig Helpers
 --------------------------------------------------------------------------------
@@ -209,7 +212,7 @@ structure PackageConfig where
 
   /--
     The root module of the package's binary executable.
-    Defaults to the package's uppercase `name`.
+    Defaults to `Main`.
 
     The root is built by recursively building its
     local imports (i.e., fellow modules of the package).
@@ -219,7 +222,7 @@ structure PackageConfig where
     there to be code (e.g., `main`) that is needed for the binary but should
     not be included in the library proper.
   -/
-  binRoot : Name := name.capitalize
+  binRoot : Name := defaultBinRoot
 
   /--
     Additional library `FileTarget`s

README.md

@@ -45,11 +45,17 @@ $ lake init hello
 
 This will initialize a git repository in the directory with a basic `.gitignore` that ignores the build directory (i.e., `build`) where Lake outputs build files.
 
-It will also create the root Lean file for the package, which uses the capitalized version of the package's name (e.g., `Hello.lean` in this example). It contains the following dummy "Hello World" program:
+It will also create the root Lean file for the package's library, which uses the capitalized version of the package's name (e.g., `Hello.lean` in this example), and the root file for the package's binary `Main.lean`. They contain the following dummy "Hello World" program split across the two files:
 
+**Hello.lean**
+```lean
+def hello := "world"
+```
+
+**Main.lean**
 ```lean
 def main : IO Unit :=
-  IO.println "Hello, world!"
+  IO.println s!"Hello, {hello}!"
 ```
 
 Lake also creates a basic `lakefile.lean` for the package:
@@ -100,6 +106,6 @@ Lake provides a large assortment of configuration options for packages.
 * `libDir`: The build subdirectory to which Lake should output the package's static library. Defaults to `lib`.
 * `binName`: The name of the package's binary executable. Defaults to the package's `name`.
 * `binDir`: The build subdirectory to which Lake should output the package's binary executable. Defaults to `bin`.
-* `binRoot`: The root module of the package's binary executable. Defaults to the package's `moduleRoot`. The root is built by recursively building its local imports (i.e., fellow modules of the package). This setting is most useful for packages that are distributing both a library and a binary (like Lake itself). In such cases, it is common for there to be code (e.g., `main`) that is needed for the binary but should not be included in the library proper.
+* `binRoot`: The root module of the package's binary executable. Defaults to `Main`. The root is built by recursively building its local imports (i.e., fellow modules of the package). This setting is most useful for packages that are distributing both a library and a binary (like Lake itself). In such cases, it is common for there to be code (e.g., `main`) that is needed for the binary but should not be included in the library proper.
 * `moreLibTargets`: Additional library `FileTarget`s (beyond the package's and its dependencies' libraries) to build and link to the package's binary executable (and/or to dependent package's executables).
 * `linkArgs`: Additional arguments to pass to `leanc` while compiling the package's binary executable. These will come *after* the paths of libraries built with `moreLibTargets`.

examples/Makefile

@@ -3,10 +3,10 @@ LAKE ?= ../build/bin/lake
 all: check-lake test time-bootstrap check-bootstrap test-bootstrapped
 
 test: test-init test-hello test-io test-deps\
-	test-git test-ffi test-ffi-dep test-main
+	test-git test-ffi test-ffi-dep
 
 clean: clean-init clean-hello clean-io clean-deps\
-	clean-git clean-ffi clean-ffi-dep clean-main clean-bootstrap
+	clean-git clean-ffi clean-ffi-dep clean-bootstrap
 
 check-lake:
 	$(LAKE) self-check
@@ -53,12 +53,6 @@ test-ffi-dep:
 clean-ffi-dep:
 	cd ffi-dep && ./clean.sh
 
-test-main:
-	cd main && ./test.sh
-
-clean-main:
-	cd main && ./clean.sh
-
 test-bootstrap:
 	cd bootstrap && ./test.sh
 

examples/deps/bar/lakefile.lean

@@ -6,4 +6,3 @@ package where
   dependencies := #[
     { name := "foo", src := Source.path (FilePath.mk ".." /  "foo") }
   ]
-  binRoot := `Main

examples/deps/foo/lakefile.lean

@@ -7,4 +7,3 @@ package where
     { name := "a", src := Source.path (FilePath.mk ".." / "a") },
     { name := "b", src := Source.path (FilePath.mk ".." / "b") }
   ]
-  binRoot := `Main

examples/ffi-dep/lakefile.lean

@@ -3,7 +3,6 @@ open System Lake DSL
 
 package where
   name := "ffi-dep"
-  binRoot := `Main
   binName := "add"
   dependencies := #[{
     name := "ffi"

examples/ffi/lakefile.lean

@@ -20,7 +20,6 @@ package (pkgDir) (args) {
   srcDir := "lib"
   libRoots := #[`Add]
   binName := "add"
-  binRoot := `Main
   -- specify the lib as an additional target
   moreLibTargets := #[cLibTarget pkgDir]
 }

examples/git/GitHello.lean

@@ -1 +0,0 @@
-import Hello

examples/git/Main.lean

@@ -0,0 +1,4 @@
+import Hello
+
+def main : IO Unit :=
+  IO.println s!"Hello, {hello}!"

examples/hello/Hello.lean

@@ -1,2 +1 @@
-def main : IO Unit :=
-  IO.println "Hello from Lake!"
+def hello := "world"

examples/hello/Main.lean

@@ -0,0 +1,4 @@
+import Hello
+
+def main : IO Unit :=
+  IO.println s!"Hello, {hello}!"

examples/main/.gitignore

@@ -1 +0,0 @@
-/build

examples/main/Lib/Foo.lean

@@ -1 +0,0 @@
-def foo := "foo"

examples/main/Main.lean

@@ -1,4 +0,0 @@
-import Lib.Foo
-
-def main :=
-  IO.println s!"Hello, {foo}!"

examples/main/clean.sh

@@ -1 +0,0 @@
-rm -rf build

examples/main/lakefile.lean

@@ -1,7 +0,0 @@
-import Lake
-open Lake DSL
-
-package where
-  name := "foo"
-  libRoots := #[`Lib]
-  binRoot := `Main

examples/main/package.sh

@@ -1 +0,0 @@
-${LAKE:-../../build/bin/lake} build-bin

examples/main/test.sh

@@ -1,5 +0,0 @@
-set -e
-
-./clean.sh
-./package.sh
-./build/bin/foo