refactor: lake: switch new/init default to TOML (#5504)

Changes the default configuration for new Lake packages to TOML.

Closes #4106.

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

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

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`.

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 <<EOF
@@ -52,7 +52,7 @@ git commit -am 'second commit in a'
 popd
 
 # c@1: require a@master, manifest a@2
-$LAKE new c lib
+$LAKE new c lib.lean
 pushd c
 git checkout -b master
 cat >>lakefile.lean <<EOF
@@ -67,7 +67,7 @@ git commit -am 'first commit in c'
 popd
 
 # d@1: require b@master c@master => 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 <<EOF

src/lake/tests/init/test.sh

@@ -38,7 +38,7 @@ done
 
 # Test default (std) template
 
-$LAKE new hello
+$LAKE new hello .lean
 $LAKE -d hello exe hello
 test -f hello/.lake/build/lib/Hello.olean
 rm -rf hello
@@ -49,7 +49,7 @@ rm -rf hello
 
 # Test exe template
 
-$LAKE new hello exe
+$LAKE new hello exe.lean
 test -f hello/Main.lean
 $LAKE -d hello exe hello
 rm -rf hello
@@ -60,7 +60,7 @@ rm -rf hello
 
 # Test lib template
 
-$LAKE new hello lib
+$LAKE new hello lib.lean
 $LAKE -d hello build Hello
 test -f hello/.lake/build/lib/Hello.olean
 rm -rf hello
@@ -71,7 +71,7 @@ rm -rf hello
 
 # Test math template
 
-$LAKE new qed math || true # ignore toolchain download errors
+$LAKE new qed math.lean || true # ignore toolchain download errors
 # Remove the require, since we do not wish to download mathlib during tests
 sed_i '/^require.*/{N;d;}' qed/lakefile.lean
 $LAKE -d qed build Qed