From 65fa1e06b2a688e9be8abbd8da4a36331480ae9b Mon Sep 17 00:00:00 2001 From: tydeu Date: Tue, 12 Sep 2023 22:18:43 -0400 Subject: [PATCH] feat: lake: improve package templates * add library directory * add note on `supportInterpreter` * use `where`-style configs --- src/lake/Lake/CLI/Init.lean | 54 ++++++++++++++----------- src/lake/Lake/Config/LeanExeConfig.lean | 9 +++-- src/lake/tests/clone/test.sh | 2 +- src/lake/tests/init/test.sh | 12 +++--- 4 files changed, 44 insertions(+), 33 deletions(-) diff --git a/src/lake/Lake/CLI/Init.lean b/src/lake/Lake/CLI/Init.lean index 580bd1d219..c2b00f62f5 100644 --- a/src/lake/Lake/CLI/Init.lean +++ b/src/lake/Lake/CLI/Init.lean @@ -22,9 +22,14 @@ s!"/{defaultBuildDir} /{defaultPackagesDir}/* " -def libFileContents := +def basicFileContents := s!"def hello := \"world\"" +def libRootFileContents (libName : String) (libRoot : String) := +s!"-- This module serves as the root of the `{libName}` library. +-- Import modules here that should be built as part of the library. +import {libRoot}.Basic" + def mainFileName : FilePath := s!"{defaultExeRoot}.lean" @@ -44,63 +49,61 @@ def stdConfigFileContents (pkgName libRoot : String) := s!"import Lake open Lake DSL -package {pkgName} \{ +package {pkgName} where -- add package configuration options here -} -lean_lib {libRoot} \{ +lean_lib {libRoot} where -- add library configuration options here -} @[default_target] -lean_exe {pkgName} \{ +lean_exe {pkgName} where root := `Main -} + -- Enables the use of the Lean interpreter by the executable (e.g., + -- `runFrontend`) at the expense of increased binary size on Linux. + -- Remove this line if you do not need such functionality. + supportInterpreter := true " def exeConfigFileContents (pkgName exeRoot : String) := s!"import Lake open Lake DSL -package {pkgName} \{ +package {pkgName} where -- add package configuration options here -} @[default_target] -lean_exe {exeRoot} \{ - -- add executable configuration options here -} +lean_exe {exeRoot} where + -- Enables the use of the Lean interpreter by the executable (e.g., + -- `runFrontend`) at the expense of increased binary size on Linux. + -- Remove this line if you do not need such functionality. + supportInterpreter := true " def libConfigFileContents (pkgName libRoot : String) := s!"import Lake open Lake DSL -package {pkgName} \{ +package {pkgName} where -- add package configuration options here -} @[default_target] -lean_lib {libRoot} \{ +lean_lib {libRoot} where -- add library configuration options here -} " def mathConfigFileContents (pkgName libRoot : String) := s!"import Lake open Lake DSL -package {pkgName} \{ +package {pkgName} where -- add any package configuration options here -} require mathlib from git \"https://github.com/leanprover-community/mathlib4.git\" @[default_target] -lean_lib {libRoot} \{ +lean_lib {libRoot} where -- add any library configuration options here -} " def mathToolchainUrl : String := @@ -164,9 +167,14 @@ def initPkg (dir : FilePath) (name : String) (tmp : InitTemplate) (env : Lake.En unless (← rootFile.pathExists) do IO.FS.writeFile rootFile exeFileContents else - if !rootExists then - IO.FS.createDirAll rootFile.parent.get! - IO.FS.writeFile rootFile libFileContents + unless rootExists do + let libDir := rootFile.withExtension "" + let basicFile := libDir / "Basic.lean" + unless (← basicFile.pathExists) do + IO.FS.createDirAll libDir + IO.FS.writeFile basicFile basicFileContents + let rootContents := libRootFileContents root.toString rootNameStr + IO.FS.writeFile rootFile rootContents if tmp = .std then let mainFile := dir / mainFileName unless (← mainFile.pathExists) do diff --git a/src/lake/Lake/Config/LeanExeConfig.lean b/src/lake/Lake/Config/LeanExeConfig.lean index 5026f7b712..d618fe610d 100644 --- a/src/lake/Lake/Config/LeanExeConfig.lean +++ b/src/lake/Lake/Config/LeanExeConfig.lean @@ -51,12 +51,13 @@ structure LeanExeConfig extends LeanConfig where nativeFacets : Array (ModuleFacet (BuildJob FilePath)) := #[Module.oFacet] /-- - Whether to expose symbols within the executable to the Lean interpreter. - This allows the executable to interpret Lean files (e.g., via - `Lean.Elab.runFrontend`). + Enables the executable to interpret Lean files (e.g., via + `Lean.Elab.runFrontend`) by exposing symbols within the executable + to the Lean interpreter. Implementation-wise, this passes `-rdynamic` to the linker when building - on non-Windows systems. + on non-Windows systems. This increases the size of the binary on Linux, so + this feature should only be enabled when necessary. Defaults to `false`. -/ diff --git a/src/lake/tests/clone/test.sh b/src/lake/tests/clone/test.sh index d1da54ad3a..ef69514563 100755 --- a/src/lake/tests/clone/test.sh +++ b/src/lake/tests/clone/test.sh @@ -44,7 +44,7 @@ $LAKE build 3>&1 1>&2 2>&3 | diff - /dev/null # Test that Lake produces a warning if local changes are made to a dependency # See https://github.com/leanprover/lake/issues/167 -sed_i "s/world/changes/" lake-packages/hello/Hello.lean +sed_i "s/world/changes/" lake-packages/hello/Hello/Basic.lean ! git -C lake-packages/hello diff --exit-code $LAKE build 3>&1 1>&2 2>&3 | grep "has local changes" ./build/bin/test | grep "Hello, changes" diff --git a/src/lake/tests/init/test.sh b/src/lake/tests/init/test.sh index 8ae8026037..7a947e71b7 100755 --- a/src/lake/tests/init/test.sh +++ b/src/lake/tests/init/test.sh @@ -7,23 +7,25 @@ LAKE=${LAKE:-../../build/bin/lake} # Test `new` and `init` with bad template (should error) -$LAKE new foo bar && exit 1 || true -$LAKE init foo bar && exit 1 || true +! $LAKE new foo bar +! $LAKE init foo bar -# Test `new` with `.` +# Test creating multi-level packages with a `.` $LAKE new hello.world $LAKE -d hello-world build hello-world/build/bin/hello-world +test -f hello-world/Hello/World/Basic.lean -# Test `new` with `-` +# Test creating packages with a `-` (i.e., a non-Lean name) # https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/lake.20new.20lean-data $LAKE new lean-data $LAKE -d lean-data build lean-data/build/bin/lean-data -# Test issue 128 +# Test creating packages with keyword names +# https://github.com/leanprover/lake/issues/128 $LAKE new meta $LAKE -d meta build