From 557adf9ffcc99b91c9d16e59f93225b089ce1cbc Mon Sep 17 00:00:00 2001 From: tydeu Date: Sat, 2 Oct 2021 23:41:55 -0400 Subject: [PATCH] refactor: default `binRoot` to `Main` and expand `init` code --- Lake/Init.lean | 28 ++++++++++++++++++++-------- Lake/Package.lean | 7 +++++-- README.md | 12 +++++++++--- examples/Makefile | 10 ++-------- examples/deps/bar/lakefile.lean | 1 - examples/deps/foo/lakefile.lean | 1 - examples/ffi-dep/lakefile.lean | 1 - examples/ffi/lakefile.lean | 1 - examples/git/GitHello.lean | 1 - examples/git/Main.lean | 4 ++++ examples/hello/Hello.lean | 3 +-- examples/hello/Main.lean | 4 ++++ examples/io/{Io.lean => Main.lean} | 0 examples/main/.gitignore | 1 - examples/main/Lib/Foo.lean | 1 - examples/main/Main.lean | 4 ---- examples/main/clean.sh | 1 - examples/main/lakefile.lean | 7 ------- examples/main/package.sh | 1 - examples/main/test.sh | 5 ----- 20 files changed, 45 insertions(+), 48 deletions(-) delete mode 100644 examples/git/GitHello.lean create mode 100644 examples/git/Main.lean create mode 100644 examples/hello/Main.lean rename examples/io/{Io.lean => Main.lean} (100%) delete mode 100644 examples/main/.gitignore delete mode 100644 examples/main/Lib/Foo.lean delete mode 100644 examples/main/Main.lean delete mode 100755 examples/main/clean.sh delete mode 100644 examples/main/lakefile.lean delete mode 100755 examples/main/package.sh delete mode 100755 examples/main/test.sh diff --git a/Lake/Init.lean b/Lake/Init.lean index e0bf7842cc..ad790ccdd7 100644 --- a/Lake/Init.lean +++ b/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" diff --git a/Lake/Package.lean b/Lake/Package.lean index 71edb41e2f..486f886ed5 100644 --- a/Lake/Package.lean +++ b/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 diff --git a/README.md b/README.md index 510e306730..54cf68abfa 100644 --- a/README.md +++ b/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`. diff --git a/examples/Makefile b/examples/Makefile index 94770580d6..c19c145998 100644 --- a/examples/Makefile +++ b/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 diff --git a/examples/deps/bar/lakefile.lean b/examples/deps/bar/lakefile.lean index 57ac9008a3..a8d02fac23 100644 --- a/examples/deps/bar/lakefile.lean +++ b/examples/deps/bar/lakefile.lean @@ -6,4 +6,3 @@ package where dependencies := #[ { name := "foo", src := Source.path (FilePath.mk ".." / "foo") } ] - binRoot := `Main diff --git a/examples/deps/foo/lakefile.lean b/examples/deps/foo/lakefile.lean index a3668bc3ae..3b11f35977 100644 --- a/examples/deps/foo/lakefile.lean +++ b/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 diff --git a/examples/ffi-dep/lakefile.lean b/examples/ffi-dep/lakefile.lean index 8185a607f3..4bc5fa03bb 100644 --- a/examples/ffi-dep/lakefile.lean +++ b/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" diff --git a/examples/ffi/lakefile.lean b/examples/ffi/lakefile.lean index 7cbcaba3db..7460b81daf 100644 --- a/examples/ffi/lakefile.lean +++ b/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] } diff --git a/examples/git/GitHello.lean b/examples/git/GitHello.lean deleted file mode 100644 index ccbbf4cfd0..0000000000 --- a/examples/git/GitHello.lean +++ /dev/null @@ -1 +0,0 @@ -import Hello diff --git a/examples/git/Main.lean b/examples/git/Main.lean new file mode 100644 index 0000000000..c68f7920a9 --- /dev/null +++ b/examples/git/Main.lean @@ -0,0 +1,4 @@ +import Hello + +def main : IO Unit := + IO.println s!"Hello, {hello}!" diff --git a/examples/hello/Hello.lean b/examples/hello/Hello.lean index f7ef46da83..99415d9d9f 100644 --- a/examples/hello/Hello.lean +++ b/examples/hello/Hello.lean @@ -1,2 +1 @@ -def main : IO Unit := - IO.println "Hello from Lake!" +def hello := "world" diff --git a/examples/hello/Main.lean b/examples/hello/Main.lean new file mode 100644 index 0000000000..c68f7920a9 --- /dev/null +++ b/examples/hello/Main.lean @@ -0,0 +1,4 @@ +import Hello + +def main : IO Unit := + IO.println s!"Hello, {hello}!" diff --git a/examples/io/Io.lean b/examples/io/Main.lean similarity index 100% rename from examples/io/Io.lean rename to examples/io/Main.lean diff --git a/examples/main/.gitignore b/examples/main/.gitignore deleted file mode 100644 index 796b96d1c4..0000000000 --- a/examples/main/.gitignore +++ /dev/null @@ -1 +0,0 @@ -/build diff --git a/examples/main/Lib/Foo.lean b/examples/main/Lib/Foo.lean deleted file mode 100644 index 9cc255c0fa..0000000000 --- a/examples/main/Lib/Foo.lean +++ /dev/null @@ -1 +0,0 @@ -def foo := "foo" diff --git a/examples/main/Main.lean b/examples/main/Main.lean deleted file mode 100644 index c70ccdbbd6..0000000000 --- a/examples/main/Main.lean +++ /dev/null @@ -1,4 +0,0 @@ -import Lib.Foo - -def main := - IO.println s!"Hello, {foo}!" diff --git a/examples/main/clean.sh b/examples/main/clean.sh deleted file mode 100755 index 1582321863..0000000000 --- a/examples/main/clean.sh +++ /dev/null @@ -1 +0,0 @@ -rm -rf build diff --git a/examples/main/lakefile.lean b/examples/main/lakefile.lean deleted file mode 100644 index 72d2c5356a..0000000000 --- a/examples/main/lakefile.lean +++ /dev/null @@ -1,7 +0,0 @@ -import Lake -open Lake DSL - -package where - name := "foo" - libRoots := #[`Lib] - binRoot := `Main diff --git a/examples/main/package.sh b/examples/main/package.sh deleted file mode 100755 index bd64051f9d..0000000000 --- a/examples/main/package.sh +++ /dev/null @@ -1 +0,0 @@ -${LAKE:-../../build/bin/lake} build-bin diff --git a/examples/main/test.sh b/examples/main/test.sh deleted file mode 100755 index 79ed78db84..0000000000 --- a/examples/main/test.sh +++ /dev/null @@ -1,5 +0,0 @@ -set -e - -./clean.sh -./package.sh -./build/bin/foo