diff --git a/src/lake/Lake/Config/Lang.lean b/src/lake/Lake/Config/Lang.lean index c831a7e036..d12e9b0fdc 100644 --- a/src/lake/Lake/Config/Lang.lean +++ b/src/lake/Lake/Config/Lang.lean @@ -10,7 +10,10 @@ inductive ConfigLang | lean | toml deriving Repr, DecidableEq -instance : Inhabited ConfigLang := ⟨.lean⟩ +/-- Lake's default configuration language. -/ +abbrev ConfigLang.default : ConfigLang := .toml + +instance : Inhabited ConfigLang := ⟨.default⟩ def ConfigLang.ofString? : String → Option ConfigLang | "lean" => some .lean diff --git a/src/lake/Lake/Load/Toml.lean b/src/lake/Lake/Load/Toml.lean index 519231a7c9..ad20492aca 100644 --- a/src/lake/Lake/Load/Toml.lean +++ b/src/lake/Lake/Load/Toml.lean @@ -270,7 +270,7 @@ protected def DependencySrc.decodeToml (t : Table) (ref := Syntax.missing) : Exc instance : DecodeToml DependencySrc := ⟨fun v => do DependencySrc.decodeToml (← v.decodeTable) v.ref⟩ protected def Dependency.decodeToml (t : Table) (ref := Syntax.missing) : Except (Array DecodeError) Dependency := ensureDecode do - let name ← stringToLegalOrSimpleName <$> t.tryDecode `name ref + let name ← stringToLegalOrSimpleName <$> t.tryDecode `name ref let rev? ← t.tryDecode? `rev let src? : Option DependencySrc ← id do if let some dir ← t.tryDecode? `path then @@ -316,6 +316,7 @@ def loadTomlConfig (dir relDir relConfigFile : FilePath) : LogIO Package := do let leanLibConfigs ← mkRBArray (·.name) <$> table.tryDecodeD `lean_lib #[] let leanExeConfigs ← mkRBArray (·.name) <$> table.tryDecodeD `lean_exe #[] let defaultTargets ← table.tryDecodeD `defaultTargets #[] + let defaultTargets := defaultTargets.map stringToLegalOrSimpleName let depConfigs ← table.tryDecodeD `require #[] return { dir, relDir, relConfigFile diff --git a/src/lake/README.md b/src/lake/README.md index 26ac5940a3..5105e32cc9 100644 --- a/src/lake/README.md +++ b/src/lake/README.md @@ -1,9 +1,9 @@ # Lake Lake (Lean Make) is the new build system and package manager for Lean 4. -With Lake, the package's configuration is written in Lean inside a dedicated `lakefile.lean` stored in the root of the package's directory. +Lake configurations can be written in Lean or TOML and are conventionally stored in a `lakefile` in the root directory of package. -Each `lakefile.lean` includes a `package` declaration (akin to `main`) which defines the package's basic configuration. It also typically includes build configurations for different targets (e.g., Lean libraries and binary executables) and Lean scripts to run on the command line (via `lake script run`). +A Lake configuration file defines the package's basic configuration. It also typically includes build configurations for different targets (e.g., Lean libraries and binary executables) and Lean scripts to run on the command line (via `lake script run`). ***This README provides information about Lake relative to the current commit. If you are looking for documentation for the Lake version shipped with a given Lean release, you should look at the README of that version.*** @@ -63,7 +63,7 @@ Hello/ # library source files; accessible via `import Hello.*` ... # additional files should be added here Hello.lean # library root; imports standard modules from Hello Main.lean # main file of the executable (contains `def main`) -lakefile.lean # Lake package configuration +lakefile.toml # Lake package configuration lean-toolchain # the Lean version used by the package .gitignore # excludes system-specific files (e.g. `build`) from Git ``` @@ -90,23 +90,21 @@ def main : IO Unit := IO.println s!"Hello, {hello}!" ``` -Lake also creates a basic `lakefile.lean` for the package along with a `lean-toolchain` file that contains the name of the Lean toolchain Lake belongs to, which tells [`elan`](https://github.com/leanprover/elan) to use that Lean toolchain for the package. +Lake also creates a basic `lakefile.toml` for the package along with a `lean-toolchain` file that contains the name of the Lean toolchain Lake belongs to, which tells [`elan`](https://github.com/leanprover/elan) to use that Lean toolchain for the package. -**lakefile.lean** -```lean -import Lake -open Lake DSL +**lakefile.toml** +```toml +name = "hello" +version = "0.1.0" +defaultTargets = ["hello"] -package «hello» where - -- add package configuration options here +[[lean_lib]] +name = "Hello" -lean_lib «Hello» where - -- add library configuration options here - -@[default_target] -lean_exe «hello» where - root := `Main +[[lean_exe]] +name = "hello" +root = "Main" ``` The command `lake build` is used to build the package (and its [dependencies](#adding-dependencies), if it has them) into a native executable. The result will be placed in `.lake/build/bin`. The command `lake clean` deletes `build`. diff --git a/src/lake/tests/depTree/test.sh b/src/lake/tests/depTree/test.sh index 5ab94d4f1e..d4d0907dc9 100755 --- a/src/lake/tests/depTree/test.sh +++ b/src/lake/tests/depTree/test.sh @@ -20,7 +20,7 @@ fi # https://github.com/leanprover/lake/issues/119 # a@1/init -$LAKE new a lib +$LAKE new a lib.lean pushd a git checkout -b master git add . @@ -31,7 +31,7 @@ git tag init popd # b@1: require a@master, manifest a@1 -$LAKE new b lib +$LAKE new b lib.lean pushd b git checkout -b master cat >>lakefile.lean <>lakefile.lean < a, manifest a@1 b@1 c@1 -$LAKE new d lib +$LAKE new d lib.lean pushd d git checkout -b master cat >>lakefile.lean <