feat: lake: alternative TOML config (#3298)

Adds an alternative TOML configuration format to Lake. 

* Uses TOML v1.0.0 and is fully specification compliant (tested via
[toml-test v1.4.0](https://github.com/toml-lang/toml-test/tree/v1.4.0)).
* Supports package configuration options, Lean libraries, Lean
executables, and dependencies.
* TOML configurations can be generated for new projects via `lake
new|init <pkg> <template>.toml`.
* Supported configurations can be converted to/from TOML via `lake
translate-config <lang>`.

src/lake/.gitignore

@@ -1,3 +1,3 @@
 .lake
 lake-manifest.json
-*produced.out
+*produced.*

src/lake/Lake.lean

@@ -8,3 +8,4 @@ import Lake.Config
 import Lake.DSL
 import Lake.Version
 import Lake.CLI.Actions
+import Lake.Toml

src/lake/Lake/Build/Topological.lean

@@ -84,7 +84,7 @@ We use `keyOf` to the derive the unique key of a fetch from its descriptor
 `a : α`. We do this because descriptors may not be comparable and/or contain
 more information than necessary to determine uniqueness.
 -/
-@[inline] partial def recFetchAcyclic [BEq κ] [Monad m]
+@[inline] def recFetchAcyclic [BEq κ] [Monad m]
 (keyOf : α → κ) (fetch : DRecFetchFn α β (CycleT κ m)) : DFetchFn α β (CycleT κ m) :=
   recFetch fun a recurse =>
     /-
@@ -110,30 +110,3 @@ memoize fetch results and thus avoid computing the same result twice.
 : DFetchFn α (fun a => β (keyOf a)) (CycleT κ m) :=
   recFetchAcyclic keyOf fun a recurse =>
     fetchOrCreate (keyOf a) do fetch a recurse
-
-/-!
-## Building
-
-In this section, we use the abstractions we have just created to define
-the desired topological recursive build function (a.k.a. a suspending scheduler).
--/
-
-/-- Recursively builds objects for the keys `κ`, avoiding cycles. -/
-@[inline] def buildAcyclic [BEq κ] [Monad m]
-(keyOf : α → κ) (a : α) (build : RecFetchFn α β (CycleT κ m)) : ExceptT (Cycle κ) m β :=
-  recFetchAcyclic (β := fun _ => β) keyOf build a []
-
-/-- Dependently typed version of `buildTop`. -/
-@[inline] def buildDTop (β) [BEq κ] [Monad m] [MonadDStore κ β m]
-(keyOf : α → κ) (a : α) (build : DRecFetchFn α (fun a => β (keyOf a)) (CycleT κ m))
-: ExceptT (Cycle κ) m (β (keyOf a)) :=
-  recFetchMemoize keyOf build a []
-
-/--
-Recursively fills a `MonadStore` of key-object pairs by
-building objects topologically (ι.e., depth-first with memoization).
-If a cycle is detected, the list of keys traversed is thrown.
--/
-@[inline] def buildTop [BEq κ] [Monad m] [MonadStore κ β m]
-(keyOf : α → κ) (a : α) (build : RecFetchFn α β (CycleT κ m)) : ExceptT (Cycle κ) m β :=
-  recFetchMemoize (β := fun _ => β) keyOf build a []

src/lake/Lake/Build/Trace.lean

@@ -3,6 +3,7 @@ Copyright (c) 2021 Mac Malone. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mac Malone
 -/
+import Lake.Util.Newline
 
 open System
 namespace Lake
@@ -128,23 +129,6 @@ def computeFileHash (file : FilePath) : IO Hash :=
 
 instance : ComputeHash FilePath IO := ⟨computeFileHash⟩
 
-/-- This is the same as `String.replace text "\r\n" "\n"`, but more efficient. -/
-@[inline] partial def crlf2lf (text : String) : String :=
-  go "" 0 0
-where
-  go (acc : String) (accStop pos : String.Pos) : String :=
-    if h : text.atEnd pos then
-      -- note: if accStop = 0 then acc is empty
-      if accStop = 0 then text else acc ++ text.extract accStop pos
-    else
-      let c := text.get' pos h
-      let pos' := text.next' pos h
-      if c == '\r' && text.get pos' == '\n' then
-        let acc := acc ++ text.extract accStop pos
-        go acc pos' (text.next pos')
-      else
-        go acc accStop pos'
-
 def computeTextFileHash (file : FilePath) : IO Hash := do
   let text ← IO.FS.readFile file
   let text := crlf2lf text

src/lake/Lake/CLI/Error.lean

@@ -18,6 +18,7 @@ inductive CliError
 | unexpectedArguments (args : List String)
 /- Init CLI Errors -/
 | unknownTemplate (spec : String)
+| unknownConfigLang (spec : String)
 /- Build CLI Errors -/
 | unknownModule (mod : Name)
 | unknownPackage (spec : String)
@@ -31,10 +32,12 @@ inductive CliError
 | invalidFacet (target : Name) (facet : Name)
 /- Executable CLI Errors -/
 | unknownExe (spec : String)
-/- Script CLI Error -/
+/- Script CLI Error  -/
 | unknownScript (script : String)
 | missingScriptDoc (script : String)
 | invalidScriptSpec (spec : String)
+/-- Translate Errors -/
+| outputConfigExists (path : System.FilePath)
 /- Config Errors -/
 | unknownLeanInstall
 | unknownLakeInstall
@@ -53,6 +56,7 @@ def toString : CliError → String
 | unknownLongOption opt   => s!"unknown long option '{opt}'"
 | unexpectedArguments as  => s!"unexpected arguments: {" ".intercalate as}"
 | unknownTemplate spec    => s!"unknown package template `{spec}`"
+| unknownConfigLang spec  => s!"unknown configuration language `{spec}`"
 | unknownModule mod       => s!"unknown module `{mod.toString false}`"
 | unknownPackage spec     => s!"unknown package `{spec}`"
 | unknownFacet ty f       => s!"unknown {ty} facet `{f.toString false}`"
@@ -67,6 +71,7 @@ def toString : CliError → String
 | unknownScript s         => s!"unknown script {s}"
 | missingScriptDoc s      => s!"no documentation provided for `{s}`"
 | invalidScriptSpec s     => s!"invalid script spec '{s}' (too many '/')"
+| outputConfigExists f    => s!"output configuration file already exists: {f}"
 | unknownLeanInstall      => "could not detect a Lean installation"
 | unknownLakeInstall      => "could not detect the configuration of the Lake installation"
 | leanRevMismatch e a     => s!"expected Lean commit {e}, but got {if a.isEmpty then "nothing" else a}"

src/lake/Lake/CLI/Help.lean

@@ -25,6 +25,7 @@ COMMANDS:
   script                manage and run workspace scripts
   scripts               shorthand for `lake script list`
   run <script>          shorthand for `lake script run`
+  translate-config      change language of the package configuration
   serve                 start the Lean language server
 
 OPTIONS:
@@ -49,21 +50,24 @@ s!"The initial configuration and starter files are based on the template:
   std                   library and executable; default
   exe                   executable only
   lib                   library only
-  math                  library only with a mathlib dependency"
+  math                  library only with a mathlib dependency
+
+Templates can be suffixed with `.lean` or `.toml` to produce a Lean or TOML
+version of the configuration file, respectively. The default is Lean."
 
 def helpNew :=
 s!"Create a Lean package in a new directory
 
 USAGE:
-  lake new <name> [<template>]
+  lake new <name> [<template>][.<language>]
 
 {templateHelp}"
 
 def helpInit :=
 s!"Create a Lean package in the current directory
 
 USAGE:
-  lake init [<name>] [<template>]
+  lake init [<name>] [<template>][.<language>]
 
 {templateHelp}
 
@@ -244,6 +248,21 @@ learn how to specify targets), builds it if it is out of date, and then runs
 it with the given `args` in Lake's environment (see `lake help env` for how
 the environment is set up)."
 
+def helpTranslateConfig :=
+"Translate a Lake configuration file into a different language
+
+USAGE:
+  lake translate-config <lang> [<out-file>]
+
+Translates the loaded package's configuration into another of
+Lake's supported configuration languages (i.e., either `lean` or `toml`).
+The produced file is written to `out-file` or, if not provided, the path of
+the configuration file with the new language's extension. If the output file
+already exists, Lake will error.
+
+Translation is lossy. It does not preserve comments or formatting and
+non-declarative configuration will be discarded."
+
 def helpScript : (cmd : String) → String
 | "list"                => helpScriptList
 | "run"                 => helpScriptRun
@@ -263,4 +282,5 @@ def help : (cmd : String) → String
 | "serve"               => helpServe
 | "env"                 => helpEnv
 | "exe" | "exec"        => helpExe
+| "translate-config"    => helpTranslateConfig
 | _                     => usage

src/lake/Lake/CLI/Init.lean

@@ -5,6 +5,7 @@ Authors: Gabriel Ebner, Sebastian Ullrich, Mac Malone
 -/
 import Lake.Util.Git
 import Lake.Util.Sugar
+import Lake.Config.Lang
 import Lake.Config.Package
 import Lake.Config.Workspace
 import Lake.Load.Config
@@ -46,7 +47,7 @@ s!"def main : IO Unit :=
   IO.println s!\"Hello, world!\"
 "
 
-def stdConfigFileContents (pkgName libRoot exeName : String) :=
+def stdLeanConfigFileContents (pkgName libRoot exeName : String) :=
 s!"import Lake
 open Lake DSL
 
@@ -61,7 +62,19 @@ lean_exe {exeName} where
   root := `Main
 "
 
-def exeConfigFileContents (pkgName exeRoot : String) :=
+def stdTomlConfigFileContents (pkgName libRoot exeName : String) :=
+s!"name = {repr pkgName}
+defaultTargets = [{repr exeName}]
+
+[[lean_lib]]
+name = {repr libRoot}
+
+[[lean_exe]]
+name = {repr exeName}
+root = \"Main\"
+"
+
+def exeLeanConfigFileContents (pkgName exeRoot : String) :=
 s!"import Lake
 open Lake DSL
 
@@ -70,13 +83,18 @@ package {pkgName} where
 
 @[default_target]
 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
+  -- add executable configuration options here
 "
 
-def libConfigFileContents (pkgName libRoot : String) :=
+def exeTomlConfigFileContents (pkgName exeRoot : String) :=
+s!"name = {repr pkgName}
+defaultTargets = [{repr exeRoot}]
+
+[[lean_exe]]
+name = {repr exeRoot}
+"
+
+def libLeanConfigFileContents (pkgName libRoot : String) :=
 s!"import Lake
 open Lake DSL
 
@@ -88,15 +106,22 @@ lean_lib {libRoot} where
   -- add library configuration options here
 "
 
-def mathConfigFileContents (pkgName libRoot : String) :=
+def libTomlConfigFileContents (pkgName libRoot : String) :=
+s!"name = {repr pkgName}
+defaultTargets = [{repr libRoot}]
+
+[[lean_lib]]
+name = {repr libRoot}
+"
+
+def mathLeanConfigFileContents (pkgName libRoot : String) :=
 s!"import Lake
 open Lake DSL
 
 package {pkgName} where
   -- Settings applied to both builds and interactive editing
   leanOptions := #[
-    ⟨`pp.unicode.fun, true⟩, -- pretty-prints `fun a ↦ b`
-    ⟨`pp.proofs.withType, false⟩
+    ⟨`pp.unicode.fun, true⟩ -- pretty-prints `fun a ↦ b`
   ]
   -- add any additional package configuration options here
 
@@ -108,17 +133,32 @@ lean_lib {libRoot} where
   -- add any library configuration options here
 "
 
+def mathTomlConfigFileContents (pkgName libRoot : String) :=
+s!"name = {repr pkgName}
+defaultTargets = [{repr libRoot}]
+
+[leanOptions]
+pp.unicode.fun = true # pretty-prints `fun a ↦ b`
+
+[[require]]
+name = \"mathlib\"
+git = \"https://github.com/leanprover-community/mathlib4.git\"
+
+[[lean_lib]]
+name = {repr libRoot}
+"
+
 def mathToolchainUrl : String :=
   "https://raw.githubusercontent.com/leanprover-community/mathlib4/master/lean-toolchain"
 
-/-- The options for the template argument to `initPkg`. -/
+/-- Lake package template identifier. -/
 inductive InitTemplate
 | std | exe | lib | math
 deriving Repr, DecidableEq
 
 instance : Inhabited InitTemplate := ⟨.std⟩
 
-def InitTemplate.parse? : String → Option InitTemplate
+def InitTemplate.ofString? : String → Option InitTemplate
 | "std" => some .std
 | "exe" => some .exe
 | "lib" => some .lib
@@ -134,15 +174,21 @@ def escapeName! : Name → String
 | .str n s          => escapeName! n ++ "." ++ escapeIdent s
 | _                 => unreachable!
 
-def InitTemplate.configFileContents (pkgName : Name) (root : String) : InitTemplate → String
-| .std => stdConfigFileContents (escapeName! pkgName) root
-  (escapeIdent <| pkgName.toStringWithSep "-" false).toLower
-| .lib => libConfigFileContents (escapeName! pkgName) root
-| .exe => exeConfigFileContents (escapeName! pkgName) root
-| .math => mathConfigFileContents (escapeName! pkgName) root
+def InitTemplate.configFileContents  (tmp : InitTemplate) (lang : ConfigLang) (pkgName : Name) (root : Name) : String :=
+  match tmp, lang with
+  | .std, .lean => stdLeanConfigFileContents (escapeName! pkgName) (escapeName! root)
+    (escapeIdent <| pkgName.toStringWithSep "-" false).toLower
+  | .std, .toml => stdTomlConfigFileContents pkgName.toString root.toString
+    (pkgName.toStringWithSep "-" false).toLower
+  | .lib, .lean => libLeanConfigFileContents (escapeName! pkgName) (escapeName! root)
+  | .lib, .toml => libTomlConfigFileContents pkgName.toString root.toString
+  | .exe, .lean => exeLeanConfigFileContents (escapeName! pkgName) (escapeName! root)
+  | .exe, .toml => exeTomlConfigFileContents pkgName.toString root.toString
+  | .math, .lean => mathLeanConfigFileContents (escapeName! pkgName) (escapeName! root)
+  | .math, .toml => mathTomlConfigFileContents pkgName.toString root.toString
 
 /-- Initialize a new Lake package in the given directory with the given name. -/
-def initPkg (dir : FilePath) (name : String) (tmp : InitTemplate) (env : Lake.Env) : LogIO PUnit := do
+def initPkg (dir : FilePath) (name : String) (tmp : InitTemplate) (lang : ConfigLang) (env : Lake.Env) : LogIO PUnit := do
   let pkgName := stringToLegalOrSimpleName name
 
   -- determine the name to use for the root
@@ -159,14 +205,15 @@ def initPkg (dir : FilePath) (name : String) (tmp : InitTemplate) (env : Lake.En
       pure (root, rootFile, ← rootFile.pathExists)
 
   -- write default configuration file
-  let configFile := dir / defaultConfigFile
+  let configFile :=  dir / match lang with
+    | .lean => defaultLeanConfigFile | .toml => defaultTomlConfigFile
   if (← configFile.pathExists) then
     error  "package already initialized"
-  let rootNameStr := escapeName! root
-  let contents := tmp.configFileContents pkgName rootNameStr
+  let contents := tmp.configFileContents lang pkgName root
   IO.FS.writeFile configFile contents
 
   -- write example code if the files do not already exist
+  let rootNameStr := escapeName! root
   if tmp = .exe then
     unless (← rootFile.pathExists) do
       createParentDirs rootFile
@@ -225,7 +272,7 @@ def validatePkgName (pkgName : String) : LogIO PUnit := do
   if pkgName.toLower ∈ ["init", "lean", "lake", "main"] then
     error "reserved package name"
 
-def init (pkgName : String) (tmp : InitTemplate) (env : Lake.Env) (cwd : FilePath := ".") : LogIO PUnit := do
+def init (pkgName : String) (tmp : InitTemplate) (lang : ConfigLang) (env : Lake.Env) (cwd : FilePath := ".") : LogIO PUnit := do
   let pkgName ← do
     if pkgName == "." then
       let path ← IO.FS.realPath cwd
@@ -237,11 +284,11 @@ def init (pkgName : String) (tmp : InitTemplate) (env : Lake.Env) (cwd : FilePat
   let pkgName := pkgName.trim
   validatePkgName pkgName
   IO.FS.createDirAll cwd
-  initPkg cwd pkgName tmp env
+  initPkg cwd pkgName tmp lang env
 
-def new (pkgName : String) (tmp : InitTemplate) (env : Lake.Env) (cwd : FilePath := ".") : LogIO PUnit := do
+def new (pkgName : String) (tmp : InitTemplate) (lang : ConfigLang)  (env : Lake.Env) (cwd : FilePath := ".") : LogIO PUnit := do
   let pkgName := pkgName.trim
   validatePkgName pkgName
   let dirName := cwd / pkgName.map fun chr => if chr == '.' then '-' else chr
   IO.FS.createDirAll dirName
-  initPkg dirName pkgName tmp env
+  initPkg dirName pkgName tmp lang env