max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

feat: lake: alternative TOML config (#3298)

Browse source 
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>`.
This commit is contained in:
Mac Malone 2024-03-27 22:35:02 -04:00 • committed by GitHub
parent 0963f3476c
commit 55b7b07c54
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
690 changed files with 8966 additions and 288 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/lake/.gitignore vendored
View file

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

1
src/lake/Lake.lean
View file

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

29
src/lake/Lake/Build/Topological.lean
View file

@ -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 []

18
src/lake/Lake/Build/Trace.lean
View file

@ -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

7
src/lake/Lake/CLI/Error.lean
View file

@ -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}"

26
src/lake/Lake/CLI/Help.lean
View file

@ -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,13 +50,16 @@ 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}"
@ -63,7 +67,7 @@ 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

99
src/lake/Lake/CLI/Init.lean
View file

@ -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

61
src/lake/Lake/CLI/Main.lean
View file

@ -13,6 +13,7 @@ import Lake.CLI.Help
import Lake.CLI.Build
import Lake.CLI.Error
import Lake.CLI.Actions
import Lake.CLI.Translate
import Lake.CLI.Serve
-- # CLI
@ -64,10 +65,10 @@ def LakeOptions.computeEnv (opts : LakeOptions) : EIO CliError Lake.Env := do
/-- Make a `LoadConfig` from a `LakeOptions`. -/
def LakeOptions.mkLoadConfig (opts : LakeOptions) : EIO CliError LoadConfig :=
return {
env := ← opts.computeEnv
rootDir := opts.rootDir
configFile := opts.rootDir / opts.configFile
configOpts := opts.configOpts
lakeEnv := ← opts.computeEnv
wsDir := opts.rootDir
relConfigFile := opts.configFile
lakeOpts := opts.configOpts
leanOpts := Lean.Options.empty
reconfigure := opts.reconfigure
}
@ -200,14 +201,29 @@ def parseScriptSpec (ws : Workspace) (spec : String) : Except CliError Script :=
| none => throw <| CliError.unknownScript spec
| _ => throw <| CliError.invalidScriptSpec spec
def parseTemplateSpec (spec : String) : Except CliError InitTemplate :=
def parseTemplateSpec (spec : String) : Except CliError InitTemplate := do
if spec.isEmpty then
pure default
else if let some tmp := InitTemplate.parse? spec then
pure tmp
return default
else if let some tmp := InitTemplate.ofString? spec.toLower then
return tmp
else
throw <| CliError.unknownTemplate spec
def parseLangSpec (spec : String) : Except CliError ConfigLang :=
if spec.isEmpty then
return default
else if let some lang := ConfigLang.ofString? spec.toLower then
return lang
else
throw <| CliError.unknownConfigLang spec
def parseTemplateLangSpec (spec : String) : Except CliError (InitTemplate × ConfigLang) := do
match spec.splitOn "." with
| [tmp, lang] => return (← parseTemplateSpec tmp, ← parseLangSpec lang)
| [tmp] => return (← parseTemplateSpec tmp, default)
| _ => return default
/-! ## Commands -/
namespace lake
@ -267,15 +283,15 @@ protected def new : CliM PUnit := do
processOptions lakeOption
let opts ← getThe LakeOptions
let name ← takeArg "package name"
let tmp ← parseTemplateSpec <| (← takeArg?).getD ""
noArgsRem do MainM.runLogIO (new name tmp (← opts.computeEnv) opts.rootDir) opts.verbosity
let (tmp, lang) ← parseTemplateLangSpec <| (← takeArg?).getD ""
noArgsRem do MainM.runLogIO (new name tmp lang (← opts.computeEnv) opts.rootDir) opts.verbosity
protected def init : CliM PUnit := do
processOptions lakeOption
let opts ← getThe LakeOptions
let name := (← takeArg?).getD "."
let tmp ← parseTemplateSpec <| (← takeArg?).getD ""
noArgsRem do MainM.runLogIO (init name tmp (← opts.computeEnv) opts.rootDir) opts.verbosity
let (tmp, lang) ← parseTemplateLangSpec <| (← takeArg?).getD ""
noArgsRem do MainM.runLogIO (init name tmp lang (← opts.computeEnv) opts.rootDir) opts.verbosity
protected def build : CliM PUnit := do
processOptions lakeOption
@ -353,10 +369,10 @@ protected def serve : CliM PUnit := do
protected def env : CliM PUnit := do
let config ← mkLoadConfig (← getThe LakeOptions)
let env ← do
if (← config.configFile.pathExists) then
if (← configFileExists config.configFile) then
pure (← loadWorkspace config).augmentedEnvVars
else
pure config.env.vars
pure config.lakeEnv.vars
if let some cmd ← takeArg? then
let child ← IO.Process.spawn {cmd, args := (← takeArgs).toArray, env}
exit <| ← child.wait
@ -375,6 +391,22 @@ protected def exe : CliM PUnit := do
let exeFile ← ws.runBuild (exe.build >>= (·.await)) <| mkBuildConfig opts
exit <| ← (env exeFile.toString args.toArray).run <| mkLakeContext ws
protected def translateConfig : CliM PUnit := do
processOptions lakeOption
let opts ← getThe LakeOptions
let cfg ← mkLoadConfig opts
let lang ← parseLangSpec (← takeArg "configuration language")
let outFile? := (← takeArg?).map FilePath.mk
noArgsRem do
Lean.searchPathRef.set cfg.lakeEnv.leanSearchPath
let (pkg, _) ← loadPackage "[root]" cfg
let outFile := outFile?.getD <| pkg.configFile.withExtension lang.fileExtension
if (← outFile.pathExists) then
throw (.outputConfigExists outFile)
IO.FS.writeFile outFile (← pkg.mkConfigString lang)
if outFile?.isNone then
IO.FS.rename pkg.configFile (pkg.configFile.addExtension "bak")
protected def selfCheck : CliM PUnit := do
processOptions lakeOption
noArgsRem do verifyInstall (← getThe LakeOptions)
@ -399,6 +431,7 @@ def lakeCli : (cmd : String) → CliM PUnit
| "serve" => lake.serve
| "env" => lake.env
| "exe" | "exec" => lake.exe
| "translate-config" => lake.translateConfig
| "self-check" => lake.selfCheck
| "help" => lake.help
| cmd => throw <| CliError.unknownCommand cmd

6
src/lake/Lake/CLI/Serve.lean
View file

@ -28,7 +28,7 @@ The `setup-file` command is used internally by Lean 4 server.
-/
def setupFile (loadConfig : LoadConfig) (path : FilePath) (imports : List String := [])
(buildConfig : BuildConfig := {}) (verbosity : Verbosity := .normal) : MainM PUnit := do
if (← loadConfig.configFile.pathExists) then
if (← configFileExists loadConfig.configFile) then
if let some errLog := (← IO.getEnv invalidConfigEnvVar) then
IO.eprint errLog
IO.eprintln s!"Invalid Lake configuration. Please restart the server after fixing the Lake configuration file."
@ -70,9 +70,9 @@ def serve (config : LoadConfig) (args : Array String) : IO UInt32 := do
pure (← LakeT.run ctx getAugmentedEnv, ws.root.moreGlobalServerArgs)
else
IO.eprintln "warning: package configuration has errors, falling back to plain `lean --server`"
pure (config.env.baseVars.push (invalidConfigEnvVar, log), #[])
pure (config.lakeEnv.baseVars.push (invalidConfigEnvVar, log), #[])
(← IO.Process.spawn {
cmd := config.env.lean.lean.toString
cmd := config.lakeEnv.lean.lean.toString
args := #["--server"] ++ moreServerArgs ++ args
env := extraEnv
}).wait

34
src/lake/Lake/CLI/Translate.lean Normal file
View file

@ -0,0 +1,34 @@
/-
Copyright (c) 2024 Mac Malone. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Mac Malone
-/
import Lake.Load.Elab
import Lake.Config.Lang
import Lake.Config.Package
import Lake.CLI.Translate.Toml
import Lake.CLI.Translate.Lean
import Lean.PrettyPrinter
namespace Lake
open Toml Lean System PrettyPrinter
private partial def descopeSyntax : Syntax → Syntax
| .ident info rawVal val preresolved =>
.ident info rawVal val.eraseMacroScopes preresolved
| .node info k args => .node info k <| args.map descopeSyntax
| stx => stx
private def descopeTSyntax (stx : TSyntax k) : TSyntax k :=
⟨descopeSyntax stx.raw⟩
def Package.mkConfigString (pkg : Package) (lang : ConfigLang) : LogIO String := do
match lang with
| .toml => pure <| ppTable pkg.mkTomlConfig
| .lean => do
let env ← importModulesUsingCache #[`Lake] {} 1024
let pp := ppModule <| descopeTSyntax <| pkg.mkLeanConfig
match (← pp.toIO {fileName := "", fileMap := default} {env} |>.toBaseIO) with
| .ok (fmt, _) => pure <| (toString fmt).trim ++ "\n"
| .error ex =>
error s!"(internal) failed to pretty print Lean configuration: {ex.toString}"

187
src/lake/Lake/CLI/Translate/Lean.lean Normal file
View file

@ -0,0 +1,187 @@
/-
Copyright (c) 2024 Mac Malone. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Mac Malone
-/
import Lake.DSL
import Lake.Config.Package
import Lean.Parser.Module
/-! # Lean Translation
Converts a declarative Lake configuration into a Lean module.
-/
namespace Lake
open DSL System Lean Syntax Parser Module
/-! ## General Helpers -/
private local instance : Quote FilePath where
quote path := quote path.toString
private local instance : BEq FilePath where
beq a b := a.normalize == b.normalize
private local instance : Quote Bool where
quote b := mkIdent <| if b then `true else `false
@[inline] def addDeclField [Quote α] (name : Name) (val : α) (fs : Array DeclField) : Array DeclField :=
fs.push <| Unhygienic.run `(declField|$(mkIdent name) := $(quote val))
@[inline] def addDeclField? [Quote α] (name : Name) (val? : Option α) (fs : Array DeclField) : Array DeclField :=
if let some val := val? then addDeclField name val fs else fs
@[inline] def addDeclFieldD [Quote α] [BEq α] (name : Name) (val : α) (default : α) (fs : Array DeclField) : Array DeclField :=
if val == default then fs else addDeclField name val fs
@[inline] def addDeclFieldNotEmpty [Quote α] (name : Name) (val : Array α) (fs : Array DeclField) : Array DeclField :=
if val.isEmpty then fs else addDeclField name val fs
/-! ## Value Encoders -/
protected def BuildType.quote : BuildType → Term
| .debug => mkCIdent ``debug
| .minSizeRel => mkCIdent ``minSizeRel
| .relWithDebInfo => mkCIdent ``relWithDebInfo
| .release => mkCIdent ``release
instance : Quote BuildType := ⟨BuildType.quote⟩
protected def Backend.quote : Backend → Term
| .c => mkCIdent ``c
| .llvm => mkCIdent ``llvm
| .default => mkCIdent ``default
instance : Quote Backend := ⟨Backend.quote⟩
def quoteLeanOptionValue : LeanOptionValue → Term
| .ofString v => quote v
| .ofBool v => quote v
| .ofNat v => quote v
private local instance : Quote LeanOptionValue := ⟨quoteLeanOptionValue⟩
def quoteLeanOption (opt : LeanOption) : Term := Unhygienic.run do
`(⟨$(quote opt.name), $(quote opt.value)⟩)
private local instance : Quote LeanOption := ⟨quoteLeanOption⟩
/-! ## Configuration Encoders -/
def WorkspaceConfig.addDeclFields (cfg : WorkspaceConfig) (fs : Array DeclField) : Array DeclField :=
addDeclFieldD `packagesDir cfg.packagesDir defaultPackagesDir fs
def LeanConfig.addDeclFields (cfg : LeanConfig) (fs : Array DeclField) : Array DeclField :=
fs
|> addDeclFieldD `buildType cfg.buildType .release
|> addDeclFieldD `backend cfg.backend .default
|> addDeclField? `platformIndependent cfg.platformIndependent
|> addDeclFieldNotEmpty `leanOptions cfg.leanOptions
|> addDeclFieldNotEmpty `moreServerOptions cfg.moreServerOptions
|> addDeclFieldNotEmpty `moreLeanArgs cfg.moreLeanArgs
|> addDeclFieldNotEmpty `weakLeanArgs cfg.weakLeanArgs
|> addDeclFieldNotEmpty `moreLeancArgs cfg.moreLeancArgs
|> addDeclFieldNotEmpty `weakLeancArgs cfg.weakLeancArgs
|> addDeclFieldNotEmpty `moreLinkArgs cfg.moreLinkArgs
|> addDeclFieldNotEmpty `weakLinkArgs cfg.weakLinkArgs
@[inline] def mkDeclValWhere? (fields : Array DeclField) : Option (TSyntax ``declValWhere) :=
if fields.isEmpty then none else Unhygienic.run `(declValWhere|where $fields*)
def PackageConfig.mkSyntax (cfg : PackageConfig) : PackageDecl := Unhygienic.run do
let declVal? := mkDeclValWhere? <|Array.empty
|> addDeclFieldD `precompileModules cfg.precompileModules false
|> addDeclFieldD `moreGlobalServerArgs cfg.moreGlobalServerArgs #[]
|> addDeclFieldD `srcDir cfg.srcDir "."
|> addDeclFieldD `buildDir cfg.buildDir defaultBuildDir
|> addDeclFieldD `leanLibDir cfg.leanLibDir defaultLeanLibDir
|> addDeclFieldD `nativeLibDir cfg.nativeLibDir defaultNativeLibDir
|> addDeclFieldD `binDir cfg.binDir defaultBinDir
|> addDeclFieldD `irDir cfg.irDir defaultIrDir
|> addDeclField? `releaseRepo (cfg.releaseRepo <|> cfg.releaseRepo?)
|> addDeclFieldD `buildArchive (cfg.buildArchive?.getD cfg.buildArchive) (defaultBuildArchive cfg.name)
|> addDeclFieldD `preferReleaseBuild cfg.preferReleaseBuild false
|> cfg.toWorkspaceConfig.addDeclFields
|> cfg.toLeanConfig.addDeclFields
`(packageDecl|package $(mkIdent cfg.name) $[$declVal?]?)
private def getEscapedNameParts? (acc : List String) : Name → Option (List String)
| Name.anonymous => if acc.isEmpty then none else some acc
| Name.str n s => do
let s ← Name.escapePart s
getEscapedNameParts? (s::acc) n
| Name.num _ _ => none
def mkNameLit? (n : Name) : Option NameLit :=
getEscapedNameParts? [] n |>.map fun ss => mkNameLit ("`" ++ ".".intercalate ss)
protected def Glob.quote (glob : Glob) : Term := Unhygienic.run do
match glob with
| .one n => return quote n
| .submodules n =>
match mkNameLit? n with
| some lit =>`($lit:name.+)
| none => return mkCApp ``submodules #[quote n]
| .andSubmodules n =>
match mkNameLit? n with
| some lit =>`($lit:name.*)
| none => return mkCApp ``andSubmodules #[quote n]
local instance : Quote Glob := ⟨Glob.quote⟩
@[inline] private def mkConfigAttrs? (defaultTarget : Bool) : Option Attributes :=
if defaultTarget then Unhygienic.run `(Term.attributes|@[default_target]) else none
protected def LeanLibConfig.mkSyntax (cfg : LeanLibConfig) (defaultTarget := false) : LeanLibDecl := Unhygienic.run do
let declVal? := mkDeclValWhere? <| Array.empty
|> addDeclFieldD `srcDir cfg.srcDir "."
|> addDeclFieldD `roots cfg.roots #[cfg.name]
|> addDeclFieldD `globs cfg.globs (cfg.roots.map .one)
|> addDeclFieldD `libName cfg.libName (cfg.name.toString (escape := false))
|> addDeclFieldD `precompileModules cfg.precompileModules false
|> addDeclFieldD `defaultFacets cfg.defaultFacets #[LeanLib.leanArtsFacet]
|> cfg.toLeanConfig.addDeclFields
let attrs? := mkConfigAttrs? defaultTarget
`(leanLibDecl|$[$attrs?:attributes]? lean_lib $(mkIdent cfg.name) $[$declVal?]?)
protected def LeanExeConfig.mkSyntax (cfg : LeanExeConfig) (defaultTarget := false) : LeanExeDecl := Unhygienic.run do
let declVal? := mkDeclValWhere? <| Array.empty
|> addDeclFieldD `srcDir cfg.srcDir "."
|> addDeclFieldD `root cfg.root cfg.name
|> addDeclFieldD `exeName cfg.exeName (cfg.name.toStringWithSep "-" (escape := false))
|> addDeclFieldD `supportInterpreter cfg.supportInterpreter false
|> cfg.toLeanConfig.addDeclFields
let attrs? := mkConfigAttrs? defaultTarget
`(leanExeDecl|$[$attrs?:attributes]? lean_exe $(mkIdent cfg.name) $[$declVal?]?)
protected def Dependency.mkSyntax (cfg : Dependency) : RequireDecl:= Unhygienic.run do
let opts? := if cfg.opts.isEmpty then none else some <| Unhygienic.run do
cfg.opts.foldM (init := mkCIdent ``NameMap.empty) fun stx opt val =>
`($stx |>.insert $(quote opt) $(quote val))
match cfg.src with
| .path dir =>
`(requireDecl|require $(mkIdent cfg.name) from $(quote dir):term $[with $opts?]?)
| .git url rev? subDir? =>
`(requireDecl|require $(mkIdent cfg.name) from git $(quote url)
$[@ $(rev?.map quote)]? $[/ $(subDir?.map quote)]? $[with $opts?]?)
/-! ## Root Encoder -/
/-- Create a Lean module that encodes the declarative configuration of the package. -/
def Package.mkLeanConfig (pkg : Package) : TSyntax ``module := Unhygienic.run do
let pkgConfig := pkg.config.mkSyntax
let defaultTargets := pkg.defaultTargets.foldl NameSet.insert NameSet.empty
let requires := pkg.depConfigs.map (·.mkSyntax)
let leanLibs := pkg.leanLibConfigs.toArray.map fun cfg =>
cfg.mkSyntax (defaultTargets.contains cfg.name)
let leanExes := pkg.leanExeConfigs.toArray.map fun cfg =>
cfg.mkSyntax (defaultTargets.contains cfg.name)
`(module|
import $(mkIdent `Lake)
open $(mkIdent `System) $(mkIdent `Lake) $(mkIdent `DSL)
$pkgConfig:command
$[$requires:command]*
$[$leanLibs:command]*
$[$leanExes:command]*
)

128
src/lake/Lake/CLI/Translate/Toml.lean Normal file
View file

@ -0,0 +1,128 @@
/-
Copyright (c) 2024 Mac Malone. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Mac Malone
-/
import Lake.Toml.Encode
import Lake.Config.Package
/-! # TOML Translation
Converts a declarative Lake configuration into a TOML table.
-/
namespace Lake
open Lean System Toml
/-! ## Helper Encoders -/
private local instance : BEq FilePath where
beq a b := a.normalize == b.normalize
instance : ToToml Backend := ⟨(toToml ·.toString)⟩
instance : SmartInsert Backend where
smartInsert k v t := match v with | .default => t | v => t.insert k (toToml v)
instance : ToToml BuildType := ⟨(toToml ·.toString)⟩
def Toml.encodeLeanOptionValue (v : LeanOptionValue) : Value :=
match v with
| .ofString s => toToml s
| .ofBool b => toToml b
| .ofNat n => toToml n
instance : ToToml LeanOptionValue := ⟨encodeLeanOptionValue⟩
def Toml.encodeLeanOptions (opts : Array LeanOption) : Table :=
opts.foldl (init := {}) fun vs ⟨k,v⟩ => vs.insert k (toToml v)
def Toml.leanOptionsEncoder : ToToml (Array LeanOption) where
toToml opts := .table .missing <| encodeLeanOptions opts
/-! ## Configuration Encoders -/
protected def WorkspaceConfig.toToml (cfg : WorkspaceConfig) (t : Table := {}) : Table :=
t.insertD `packagesDir cfg.packagesDir defaultPackagesDir
instance : ToToml WorkspaceConfig := ⟨(toToml ·.toToml)⟩
def LeanConfig.toToml (cfg : LeanConfig) (t : Table := {}) : Table :=
have : ToToml (Array LeanOption) := leanOptionsEncoder
t.insertD `buildType cfg.buildType .release
|>.smartInsert `backend cfg.backend
|>.smartInsert `platformIndependent cfg.platformIndependent
|>.smartInsert `leanOptions cfg.leanOptions
|>.smartInsert `moreServerOptions cfg.moreServerOptions
|>.smartInsert `moreLeanArgs cfg.moreLeanArgs
|>.smartInsert `weakLeanArgs cfg.weakLeanArgs
|>.smartInsert `moreLeancArgs cfg.moreLeancArgs
|>.smartInsert `weakLeancArgs cfg.weakLeancArgs
|>.smartInsert `moreLinkArgs cfg.moreLinkArgs
|>.smartInsert `weakLinkArgs cfg.weakLinkArgs
instance : ToToml LeanConfig := ⟨(toToml ·.toToml)⟩
protected def PackageConfig.toToml (cfg : PackageConfig) (t : Table := {}) : Table :=
t.insert `name cfg.name
|>.insertD `precompileModules cfg.precompileModules false
|>.smartInsert `moreGlobalServerArgs cfg.moreGlobalServerArgs
|>.insertD `srcDir cfg.srcDir "."
|>.insertD `buildDir cfg.buildDir defaultBuildDir
|>.insertD `leanLibDir cfg.leanLibDir defaultLeanLibDir
|>.insertD `nativeLibDir cfg.nativeLibDir defaultNativeLibDir
|>.insertD `binDir cfg.binDir defaultBinDir
|>.insertD `irDir cfg.irDir defaultIrDir
|>.smartInsert `releaseRepo (cfg.releaseRepo <|> cfg.releaseRepo?)
|>.insertD `buildArchive (cfg.buildArchive?.getD cfg.buildArchive) (defaultBuildArchive cfg.name)
|>.insertD `preferReleaseBuild cfg.preferReleaseBuild false
|> cfg.toWorkspaceConfig.toToml
|> cfg.toLeanConfig.toToml
instance : ToToml PackageConfig := ⟨(toToml ·.toToml)⟩
instance : ToToml Glob := ⟨(toToml ·.toString)⟩
protected def LeanLibConfig.toToml (cfg : LeanLibConfig) (t : Table := {}) : Table :=
t.insert `name cfg.name
|>.insertD `srcDir cfg.srcDir "."
|>.insertD `roots cfg.roots #[cfg.name]
|>.insertD `globs cfg.globs (cfg.roots.map .one)
|>.insertD `libName cfg.libName (cfg.name.toString (escape := false))
|>.insertD `precompileModules cfg.precompileModules false
|>.insertD `defaultFacets cfg.defaultFacets #[LeanLib.leanArtsFacet]
|> cfg.toLeanConfig.toToml
instance : ToToml LeanLibConfig := ⟨(toToml ·.toToml)⟩
protected def LeanExeConfig.toToml (cfg : LeanExeConfig) (t : Table := {}) : Table :=
t.insert `name cfg.name
|>.insertD `srcDir cfg.srcDir "."
|>.insertD `root cfg.root cfg.name
|>.insertD `exeName cfg.exeName (cfg.name.toStringWithSep "-" (escape := false))
|>.insertD `supportInterpreter cfg.supportInterpreter false
|> cfg.toLeanConfig.toToml
instance : ToToml LeanExeConfig := ⟨(toToml ·.toToml)⟩
protected def Dependency.toToml (dep : Dependency) (t : Table := {}) : Table :=
let t := t.insert `name dep.name
let t :=
match dep.src with
| .path dir => t.insert `path (toToml dir)
| .git url rev subDir? =>
t.insert `git url
|>.smartInsert `rev rev
|>.smartInsert `subDir subDir?
t.smartInsert `options <| dep.opts.fold (·.insert · ·) Table.empty
instance : ToToml Dependency := ⟨(toToml ·.toToml)⟩
/-! ## Root Encoder -/
/-- Create a TOML table that encodes the declarative configuration of the package. -/
def Package.mkTomlConfig (pkg : Package) (t : Table := {}) : Table :=
pkg.config.toToml t
|>.smartInsert `defaultTargets pkg.defaultTargets
|>.smartInsert `require pkg.depConfigs
|>.smartInsert `lean_lib pkg.leanLibConfigs.toArray
|>.smartInsert `lean_exe pkg.leanExeConfigs.toArray

12
src/lake/Lake/Config/Defaults.lean
View file

@ -14,10 +14,16 @@ Currently not configurable.
def defaultLakeDir : FilePath := ".lake"
/-- The default setting for a `WorkspaceConfig`'s `packagesDir` option. -/
def defaultPackagesDir : FilePath := "packages"
def defaultPackagesDir := defaultLakeDir / "packages"
/-- The default name of the Lake configuration file (i.e., `lakefile.lean`). -/
def defaultConfigFile : FilePath := "lakefile.lean"
/-- The default name of the Lake configuration file (i.e., `lakefile`). -/
def defaultConfigFile : FilePath := "lakefile"
/-- The default name of the Lean Lake configuration file (i.e., `lakefile.lean`). -/
def defaultLeanConfigFile : FilePath := defaultConfigFile |>.addExtension "lean"
/-- The default name of the TOML Lake configuration file (i.e., `lakefile.toml`). -/
def defaultTomlConfigFile : FilePath := defaultConfigFile |>.addExtension "toml"
/-- The default name of the Lake manifest file (i.e., `lake-manifest.json`). -/
def defaultManifestFile : FilePath := "lake-manifest.json"

18
src/lake/Lake/Config/Glob.lean
View file

@ -19,12 +19,28 @@ inductive Glob
| submodules : Name → Glob
/-- Selects the specified module and all submodules. -/
| andSubmodules : Name → Glob
deriving Inhabited, Repr
deriving Inhabited, Repr, DecidableEq
instance : Coe Name Glob := ⟨Glob.one⟩
instance : Coe Glob (Array Glob) := ⟨Array.singleton⟩
/-- A name glob which matches all names with the prefix, including itself. -/
scoped macro:max n:name noWs ".*" : term =>
``(Glob.andSubmodules $(⟨Lean.mkNode `Lean.Parser.Term.quotedName #[n]⟩))
/-- A name glob which matches all names with the prefix, but not the prefix itself. -/
scoped macro:max n:name noWs ".+" : term =>
``(Glob.submodules $(⟨Lean.mkNode `Lean.Parser.Term.quotedName #[n]⟩))
namespace Glob
protected def toString : Glob → String
| .one n => n.toString
| .submodules n => n.toString ++ ".+"
| .andSubmodules n => n.toString ++ ".*"
instance : ToString Glob := ⟨Glob.toString⟩
def «matches» (m : Name) : (self : Glob) → Bool
| one n => n == m
| submodules n => n.isPrefixOf m && n != m

24
src/lake/Lake/Config/Lang.lean Normal file
View file

@ -0,0 +1,24 @@
/-
Copyright (c) 2024 Mac Malone. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Mac Malone
-/
namespace Lake
/-- Lake configuration language identifier. -/
inductive ConfigLang
| lean | toml
deriving Repr, DecidableEq
instance : Inhabited ConfigLang := ⟨.lean⟩
def ConfigLang.ofString? : String → Option ConfigLang
| "lean" => some .lean
| "toml" => some .toml
| _ => none
def ConfigLang.fileExtension : ConfigLang → String
| .lean => "lean"
| .toml => "toml"
instance : ToString ConfigLang := ⟨ConfigLang.fileExtension⟩

37
src/lake/Lake/Config/LeanConfig.lean
View file

@ -61,7 +61,24 @@ inductive Backend
Use the default backend. Can be overridden by more specific configuration.
-/
| default
deriving Inhabited, Repr, DecidableEq
deriving Repr, DecidableEq
instance : Inhabited Backend := ⟨.default⟩
def Backend.ofString? (s : String) : Option Backend :=
match s with
| "c" => some .c
| "llvm" => some .llvm
| "default" => some .default
| _ => none
protected def Backend.toString (bt : Backend) : String :=
match bt with
| .c => "c"
| .llvm => "llvm"
| .default => "default"
instance : ToString Backend := ⟨Backend.toString⟩
/--
If the left backend is default, choose the right one.
@ -74,7 +91,6 @@ def Backend.orPreferLeft : Backend → Backend → Backend
| .default, b => b
| b, _ => b
/-- The arguments to pass to `leanc` based on the build type. -/
def BuildType.leancArgs : BuildType → Array String
| debug => #["-Og", "-g"]
@ -82,6 +98,23 @@ def BuildType.leancArgs : BuildType → Array String
| minSizeRel => #["-Os", "-DNDEBUG"]
| release => #["-O3", "-DNDEBUG"]
def BuildType.ofString? (s : String) : Option BuildType :=
match s with
| "debug" => some .debug
| "relWithDebInfo" => some .relWithDebInfo
| "minSizeRel" => some .minSizeRel
| "release" => some .release
| _ => none
protected def BuildType.toString (bt : BuildType) : String :=
match bt with
| .debug => "debug"
| .relWithDebInfo => "relWithDebInfo"
| .minSizeRel => "minSizeRel"
| .release => "release"
instance : ToString BuildType := ⟨BuildType.toString⟩
/-- Option that is used by Lean as if it was passed using `-D`. -/
structure LeanOption where
name : Lean.Name

22
src/lake/Lake/Config/Package.lean
View file

@ -27,6 +27,11 @@ Currently used for package and target names taken from the CLI.
def stringToLegalOrSimpleName (s : String) : Name :=
if s.toName.isAnonymous then Lean.Name.mkSimple s else s.toName
/-- The default `buildArchive` configuration for a package with `name`. -/
@[inline] def defaultBuildArchive (name : Name) : String :=
s!"{name.toString false}-{System.Platform.target}.tar.gz"
--------------------------------------------------------------------------------
/-! # PackageConfig -/
--------------------------------------------------------------------------------
@ -141,8 +146,7 @@ structure PackageConfig extends WorkspaceConfig, LeanConfig where
Defaults to `{(pkg-)name}-{System.Platform.target}.tar.gz`.
-/
buildArchive : String :=
if let some name := buildArchive? then name else
s!"{name.toString false}-{System.Platform.target}.tar.gz"
if let some name := buildArchive? then name else defaultBuildArchive name
/--
Whether to prefer downloading a prebuilt release (from GitHub) rather than
@ -167,18 +171,16 @@ structure Package where
relDir : FilePath
/-- The package's user-defined configuration. -/
config : PackageConfig
/-- The elaboration environment of the package's configuration file. -/
configEnv : Environment
/-- The Lean `Options` the package configuration was elaborated with. -/
leanOpts : Options
/-- The path to the package's configuration file. -/
configFile : FilePath
/-- The path to the package's configuration file (relative to `dir`). -/
relConfigFile : FilePath
/-- The path to the package's JSON manifest of remote dependencies (relative to `dir`). -/
relManifestFile : FilePath := config.manifestFile.getD defaultManifestFile
/-- The URL to this package's Git remote. -/
remoteUrl? : Option String := none
/-- (Opaque references to) the package's direct dependencies. -/
opaqueDeps : Array OpaquePackage := #[]
/-- Dependency configurations for the package. -/
depConfigs : Array Dependency := #[]
/-- Lean library configurations for the package. -/
leanLibConfigs : OrdNameMap LeanLibConfig := {}
/-- Lean binary executable configurations for the package. -/
@ -271,6 +273,10 @@ namespace Package
@[inline] def pkgsDir (self : Package) : FilePath :=
self.dir / self.relPkgsDir
/-- The full path to the package's configuration file. -/
@[inline] def configFile (self : Package) : FilePath :=
self.dir / self.relConfigFile
/-- The path to the package's JSON manifest of remote dependencies. -/
@[inline] def manifestFile (self : Package) : FilePath :=
self.dir / self.relManifestFile

4
src/lake/Lake/Config/WorkspaceConfig.lean
View file

@ -12,7 +12,7 @@ namespace Lake
structure WorkspaceConfig where
/--
The directory to which Lake should download remote dependencies.
Defaults to `defaultLakeDir / defaultPackagesDir` (i.e., `.lake/packages`).
Defaults to `defaultPackagesDir` (i.e., `.lake/packages`).
-/
packagesDir : FilePath := defaultLakeDir / defaultPackagesDir
packagesDir : FilePath := defaultPackagesDir
deriving Inhabited, Repr

5
src/lake/Lake/DSL/DeclUtil.lean
View file

@ -25,8 +25,11 @@ def expandAttrs (attrs? : Option Attributes) : Array AttrInstance :=
else
#[]
/-- A single field assignment in a declarative configuration. -/
syntax declField :=
ident ":=" term
ident " := " term
@[inherit_doc declField] abbrev DeclField := TSyntax ``declField
syntax structVal :=
"{" manyIndent(group(declField ", "?)) "}"

8
src/lake/Lake/DSL/Meta.lean
View file

@ -5,6 +5,7 @@ Authors: Mac Malone
-/
import Lean.Elab.Eval
import Lean.Elab.ElabRules
import Lake.Util.FilePath
/-!
Syntax for elaboration time control flow.
@ -95,10 +96,3 @@ def elabRunIO : TermElab := fun stx expectedType? =>
| .ok x => return x
| .error e => throwErrorAt tk e.toString
| _ => Elab.throwUnsupportedSyntax
/-! ## ToExpr Instances -/
instance : ToExpr System.FilePath where
toExpr p := mkApp (mkConst ``System.FilePath.mk) (toExpr p.toString)
toTypeExpr := mkConst ``System.FilePath

5
src/lake/Lake/DSL/Package.lean
View file

@ -37,6 +37,11 @@ doc?:optional(docComment) attrs?:optional(Term.attributes)
let attrs := #[attr] ++ expandAttrs attrs?
mkConfigDecl packageDeclName doc? attrs ty sig
abbrev PackageDecl := TSyntax ``packageDecl
instance : Coe PackageDecl Command where
coe x := ⟨x.raw⟩
/--
Declare a post-`lake update` hook for the package.

5
src/lake/Lake/DSL/Require.lean
View file

@ -55,3 +55,8 @@ required to disambiguate the syntax).
-/
scoped macro (name := requireDecl) "require " spec:depSpec : command =>
expandDepSpec spec
@[inherit_doc requireDecl] abbrev RequireDecl := TSyntax ``requireDecl
instance : Coe RequireDecl Command where
coe x := ⟨x.raw⟩

9
src/lake/Lake/DSL/Targets.lean
View file

@ -163,6 +163,11 @@ doc?:optional(docComment) attrs?:optional(Term.attributes)
let attrs := #[attr] ++ expandAttrs attrs?
mkConfigDecl none doc? attrs ty sig
@[inherit_doc leanLibDecl] abbrev LeanLibDecl := TSyntax ``leanLibDecl
instance : Coe LeanLibDecl Command where
coe x := ⟨x.raw⟩
/--
Define a new Lean binary executable target for the package.
Can optionally be provided with a configuration of type `LeanExeConfig`.
@ -182,6 +187,10 @@ doc?:optional(docComment) attrs?:optional(Term.attributes)
let attrs := #[attr] ++ expandAttrs attrs?
mkConfigDecl none doc? attrs ty sig
@[inherit_doc leanExeDecl] abbrev LeanExeDecl := TSyntax ``leanExeDecl
instance : Coe LeanExeDecl Command where
coe x := ⟨x.raw⟩
--------------------------------------------------------------------------------
/-! ## External Library Target Declaration -/

30
src/lake/Lake/Load/Config.lean
View file

@ -15,14 +15,30 @@ open System Lean
/-- Context for loading a Lake configuration. -/
structure LoadConfig where
/-- The Lake environment of the load process. -/
env : Lake.Env
/-- The root directory of the loaded package (and its workspace). -/
rootDir : FilePath
/-- The Lean file with the package's Lake configuration (e.g., `lakefile.lean`) -/
configFile : FilePath := rootDir / defaultConfigFile
lakeEnv : Lake.Env
/-- The root directory of the Lake workspace. -/
wsDir : FilePath
/-- The directory of the loaded package (relative to the root). -/
relPkgDir : FilePath := "."
/-- The package's Lake configuration file (relative to the package directory). -/
relConfigFile : FilePath := defaultConfigFile
/-- A set of key-value Lake configuration options (i.e., `-K` settings). -/
configOpts : NameMap String := {}
lakeOpts : NameMap String := {}
/-- The Lean options with which to elaborate the configuration file. -/
leanOpts : Options := {}
/-- If true, Lake will elaborate configuration files instead of using OLeans. -/
/-- If `true`, Lake will elaborate configuration files instead of using OLeans. -/
reconfigure : Bool := false
/-- The URL to this package's Git remote (if any). -/
remoteUrl? : Option String := none
/-- The full path to loaded package's directory. -/
@[inline] def LoadConfig.pkgDir (cfg : LoadConfig) : FilePath :=
cfg.wsDir / cfg.relPkgDir
/-- The full path to loaded package's configuration file. -/
@[inline] def LoadConfig.configFile (cfg : LoadConfig) : FilePath :=
cfg.pkgDir / cfg.relConfigFile
/-- The package's Lake directory (for Lake temporary files). -/
@[inline] def LoadConfig.lakeDir (cfg : LoadConfig) : FilePath :=
cfg.pkgDir / defaultLakeDir

31
src/lake/Lake/Load/Elab.lean
View file

@ -42,7 +42,7 @@ def configModuleName : Name := `lakefile
/-- Elaborate `configFile` with the given package directory and options. -/
def elabConfigFile (pkgDir : FilePath) (lakeOpts : NameMap String)
(leanOpts := Options.empty) (configFile := pkgDir / defaultConfigFile) : LogIO Environment := do
(leanOpts := Options.empty) (configFile := pkgDir / defaultLeanConfigFile) : LogIO Environment := do
-- Read file and initialize environment
let input ← IO.FS.readFile configFile
@ -156,13 +156,12 @@ Import the `.olean` for the configuration file if `reconfigure` is not set and
an up-to-date one exists (i.e., one with matching configuration and on the same
toolchain). Otherwise, elaborate the configuration and save it to the `.olean`.
-/
def importConfigFile (pkgDir lakeDir : FilePath) (lakeEnv : Lake.Env) (lakeOpts : NameMap String)
(leanOpts := Options.empty) (configFile := pkgDir / defaultConfigFile) (reconfigure := true) : LogIO Environment := do
let some configName := FilePath.mk <$> configFile.fileName
def importConfigFile (cfg : LoadConfig) : LogIO Environment := do
let some configName := FilePath.mk <$> cfg.configFile.fileName
| error "invalid configuration file name"
let olean := lakeDir / configName.withExtension "olean"
let traceFile := lakeDir / configName.withExtension "olean.trace"
let lockFile := lakeDir / configName.withExtension "olean.lock"
let olean := cfg.lakeDir / configName.withExtension "olean"
let traceFile := cfg.lakeDir / configName.withExtension "olean.trace"
let lockFile := cfg.lakeDir / configName.withExtension "olean.lock"
/-
Remark:
To prevent race conditions between the `.olean` and its trace file
@ -206,7 +205,7 @@ def importConfigFile (pkgDir lakeDir : FilePath) (lakeEnv : Lake.Env) (lakeOpts
h.unlock
error <| s!"could not acquire an exclusive configuration lock; " ++
"another process may already be reconfiguring the package"
let configHash ← computeTextFileHash configFile
let configHash ← computeTextFileHash cfg.configFile
let elabConfig h (lakeOpts : NameMap String) : LogIO Environment := id do
/-
Remark:
@ -222,10 +221,10 @@ def importConfigFile (pkgDir lakeDir : FilePath) (lakeEnv : Lake.Env) (lakeOpts
match (← IO.FS.removeFile olean |>.toBaseIO) with
| .ok _ | .error (.noFileOrDirectory ..) =>
h.putStrLn <| Json.pretty <| toJson
{platform := System.Platform.target, leanHash := lakeEnv.leanGithash,
{platform := System.Platform.target, leanHash := cfg.lakeEnv.leanGithash,
configHash, options := lakeOpts : ConfigTrace}
h.truncate
let env ← elabConfigFile pkgDir lakeOpts leanOpts configFile
let env ← elabConfigFile cfg.pkgDir lakeOpts cfg.leanOpts cfg.configFile
Lean.writeModule env olean
h.unlock
return env
@ -235,8 +234,8 @@ def importConfigFile (pkgDir lakeDir : FilePath) (lakeEnv : Lake.Env) (lakeOpts
IO.FS.removeFile traceFile
failure
let validateTrace h : LogIO Environment := id do
if reconfigure then
elabConfig (← acquireTrace h) lakeOpts
if cfg.reconfigure then
elabConfig (← acquireTrace h) cfg.lakeOpts
else
h.lock (exclusive := false)
let contents ← h.readToEnd
@ -244,9 +243,9 @@ def importConfigFile (pkgDir lakeDir : FilePath) (lakeEnv : Lake.Env) (lakeOpts
| error "compiled configuration is invalid; run with '-R' to reconfigure"
let upToDate :=
(← olean.pathExists) ∧ trace.platform = System.Platform.target ∧
trace.leanHash = lakeEnv.leanGithash ∧ trace.configHash = configHash
trace.leanHash = cfg.lakeEnv.leanGithash ∧ trace.configHash = configHash
if upToDate then
let env ← importConfigFileCore olean leanOpts
let env ← importConfigFileCore olean cfg.leanOpts
h.unlock
return env
else
@ -254,10 +253,10 @@ def importConfigFile (pkgDir lakeDir : FilePath) (lakeEnv : Lake.Env) (lakeOpts
if (← traceFile.pathExists) then
validateTrace <| ← IO.FS.Handle.mk traceFile .read
else
IO.FS.createDirAll lakeDir
IO.FS.createDirAll cfg.lakeDir
match (← IO.FS.Handle.mk traceFile .writeNew |>.toBaseIO) with
| .ok h =>
h.lock; elabConfig h lakeOpts
h.lock; elabConfig h cfg.lakeOpts
| .error (.alreadyExists ..) =>
validateTrace <| ← IO.FS.Handle.mk traceFile .read
| .error e => error e.toString

254
src/lake/Lake/Load/Main.lean
View file

@ -13,6 +13,7 @@ import Lake.Build.Library
import Lake.Load.Materialize
import Lake.Load.Package
import Lake.Load.Elab
import Lake.Load.Toml
open System Lean
@ -22,76 +23,115 @@ The main definitions for loading a workspace and resolving dependencies.
namespace Lake
/-- Load the tagged `Dependency` definitions from a package configuration environment. -/
def loadDepsFromEnv (env : Environment) (opts : Options) : Except String (Array Dependency) := do
(packageDepAttr.getAllEntries env).mapM (evalConstCheck env opts Dependency ``Dependency)
/--
Elaborate a dependency's configuration file into a `Package`.
Elaborate a dependency's Lean configuration file into a `Package`.
The resulting package does not yet include any dependencies.
-/
def MaterializedDep.loadPackage (dep : MaterializedDep)
(wsDir : FilePath) (lakeEnv : Lake.Env) (leanOpts : Options) (reconfigure : Bool) : LogIO Package := do
let dir := wsDir / dep.relPkgDir
let lakeDir := dir / defaultLakeDir
let configEnv ← importConfigFile dir lakeDir lakeEnv dep.configOpts leanOpts (dir / dep.configFile) reconfigure
let config ← IO.ofExcept <| PackageConfig.loadFromEnv configEnv leanOpts
return {
dir
relDir := dep.relPkgDir
config, configEnv, leanOpts
configFile := dep.configFile
def loadLeanConfig (cfg : LoadConfig)
: LogIO (Package × Environment) := do
let configEnv ← importConfigFile cfg
let pkgConfig ← IO.ofExcept <| PackageConfig.loadFromEnv configEnv cfg.leanOpts
let pkg : Package := {
dir := cfg.pkgDir
relDir := cfg.relPkgDir
config := pkgConfig
relConfigFile := cfg.relConfigFile
remoteUrl? := cfg.remoteUrl?
}
return (← pkg.loadFromEnv configEnv cfg.leanOpts, configEnv)
/--
Return whether a configuration file with the given name
and/or a supported extension exists.
-/
def configFileExists (cfgFile : FilePath) : BaseIO Bool :=
if cfgFile.extension.isSome then
cfgFile.pathExists
else
let leanFile := cfgFile.addExtension "lean"
let tomlFile := cfgFile.addExtension "toml"
leanFile.pathExists <||> tomlFile.pathExists
/-- Loads a Lake package configuration (either Lean or TOML). -/
def loadPackage
(name : String) (cfg : LoadConfig)
: LogIO (Package × Option Environment) := do
if let some ext := cfg.relConfigFile.extension then
unless (← cfg.configFile.pathExists) do
error s!"{name}: configuration file not found: {cfg.configFile}"
match ext with
| "lean" => (·.map id some) <$> loadLeanConfig cfg
| "toml" => ((·,none)) <$> loadTomlConfig cfg.pkgDir cfg.relPkgDir cfg.relConfigFile
| _ => error s!"{name}: configuration has unsupported file extension: {cfg.configFile}"
else
let relLeanFile := cfg.relConfigFile.addExtension "lean"
let relTomlFile := cfg.relConfigFile.addExtension "toml"
let leanFile := cfg.pkgDir / relLeanFile
let tomlFile := cfg.pkgDir / relTomlFile
let leanExists ← leanFile.pathExists
let tomlExists ← tomlFile.pathExists
if leanExists then
if tomlExists then
logInfo s!"{name}: {relLeanFile} and {relTomlFile} are both present; using {relLeanFile}"
(·.map id some) <$> loadLeanConfig {cfg with relConfigFile := relLeanFile}
else
if tomlExists then
((·,none)) <$> loadTomlConfig cfg.pkgDir cfg.relPkgDir relTomlFile
else
error s!"{name}: no configuration file with a supported extension:\n{leanFile}\n{tomlFile}"
/--
Loads the package configuration of a materialized dependency.
Adds the facets defined in the package to the `Workspace`.
-/
def loadDepPackage
(dep : MaterializedDep) (leanOpts : Options) (reconfigure : Bool)
: StateT Workspace LogIO Package := fun ws => do
let name := dep.name.toString (escape := false)
let (pkg, env?) ← loadPackage name {
lakeEnv := ws.lakeEnv
wsDir := ws.dir
relPkgDir := dep.relPkgDir
relConfigFile := dep.configFile
lakeOpts := dep.configOpts
leanOpts
reconfigure
remoteUrl? := dep.remoteUrl?
}
if let some env := env? then
let ws ← IO.ofExcept <| ws.addFacetsFromEnv env leanOpts
return (pkg, ws)
else
return (pkg, ws)
/--
Load a `Workspace` for a Lake package by elaborating its configuration file.
Does not resolve dependencies.
-/
def loadWorkspaceRoot (config : LoadConfig) : LogIO Workspace := do
Lean.searchPathRef.set config.env.leanSearchPath
let configEnv ← importConfigFile
config.rootDir (config.rootDir / defaultLakeDir) config.env
config.configOpts config.leanOpts config.configFile config.reconfigure
let pkgConfig ← IO.ofExcept <| PackageConfig.loadFromEnv configEnv config.leanOpts
let root := {
dir := config.rootDir
relDir := "."
config := pkgConfig
configEnv
leanOpts := config.leanOpts
configFile := config.configFile
}
return {
root, lakeEnv := config.env
Lean.searchPathRef.set config.lakeEnv.leanSearchPath
let (root, env?) ← loadPackage "[root]" config
let ws : Workspace := {
root, lakeEnv := config.lakeEnv
moduleFacetConfigs := initModuleFacetConfigs
packageFacetConfigs := initPackageFacetConfigs
libraryFacetConfigs := initLibraryFacetConfigs
}
if let some env := env? then
IO.ofExcept <| ws.addFacetsFromEnv env config.leanOpts
else
return ws
/--
Finalize the workspace's root and its transitive dependencies
and add them to the workspace.
-/
def Workspace.finalize (ws : Workspace) : LogIO Workspace := do
have : MonadStore Name Package (StateT Workspace LogIO) := {
fetch? := fun name => return (← get).findPackage? name
store := fun _ pkg => modify (·.addPackage pkg)
}
let (res, ws) ← EStateT.run ws do
buildTop (·.name) ws.root fun pkg load => do
let depPkgs ← pkg.deps.mapM load
set <| ← IO.ofExcept <| (← get).addFacetsFromEnv pkg.configEnv pkg.leanOpts
let pkg ← pkg.finalize depPkgs
return pkg
match res with
| Except.ok root =>
return {ws with root}
| Except.error cycle => do
/-- Recursively visits a package dependency graph, avoiding cycles. -/
private def resolveDepsAcyclic
[Monad m] [MonadError m]
(root : Package) (f : RecFetchFn Package α (CycleT Name m))
: m α := do
match (← ExceptT.run <| recFetchAcyclic (·.name) f root []) with
| .ok s => pure s
| .error cycle =>
let cycle := cycle.map (s!" {·}")
error <|
s!"oops! dependency load cycle detected (this likely indicates a bug in Lake):\n" ++
"\n".intercalate cycle
error s!"dependency cycle detected:\n{"\n".intercalate cycle}"
/--
Rebuild the workspace's Lake manifest and materialize missing dependencies.
@ -103,11 +143,15 @@ root dependencies. Otherwise, only update the root dependencies specified.
If `reconfigure`, elaborate configuration files while updating, do not use OLeans.
-/
def Workspace.updateAndMaterialize (ws : Workspace)
(toUpdate : NameSet := {}) (reconfigure := true) : LogIO Workspace := do
let res ← StateT.run (s := mkNameMap MaterializedDep) <|
StateT.run' (s := mkNameMap PackageEntry) <| EStateT.run' (mkNameMap Package) do
def Workspace.updateAndMaterialize
(ws : Workspace) (leanOpts : Options := {})
(toUpdate : NameSet := {}) (reconfigure := true)
: LogIO Workspace := do
let ((root, deps), ws) ←
StateT.run (s := ws) <| StateT.run (s := mkNameMap MaterializedDep) <|
StateT.run' (s := mkNameMap PackageEntry) <| StateT.run' (s := mkNameMap Package) do
-- Use manifest versions of root packages that should not be updated
let rootName := ws.root.name.toString (escape := false)
match (← Manifest.load ws.manifestFile |>.toBaseIO) with
| .ok manifest =>
unless toUpdate.isEmpty do
@ -122,19 +166,18 @@ def Workspace.updateAndMaterialize (ws : Workspace)
IO.FS.rename oldPkgsDir ws.pkgsDir
if let .error e ← doRename.toBaseIO then
error <|
s!"{ws.root.name}: could not rename packages directory " ++
s!"{rootName}: could not rename packages directory " ++
s!"({oldPkgsDir} -> {ws.pkgsDir}): {e}"
| .error (.noFileOrDirectory ..) =>
logInfo s!"{ws.root.name}: no previous manifest, creating one from scratch"
logInfo s!"{rootName}: no previous manifest, creating one from scratch"
| .error e =>
unless toUpdate.isEmpty do
liftM (m := IO) <| throw e -- only ignore manifest on a bare `lake update`
logWarning s!"{ws.root.name}: ignoring previous manifest because it failed to load: {e}"
buildAcyclic (·.name) ws.root fun pkg resolve => do
logWarning s!"{rootName}: ignoring previous manifest because it failed to load: {e}"
resolveDepsAcyclic ws.root fun pkg resolve => do
let inherited := pkg.name != ws.root.name
-- Materialize this package's dependencies first
let deps ← IO.ofExcept <| loadDepsFromEnv pkg.configEnv pkg.leanOpts
let deps ← deps.mapM fun dep => fetchOrCreate dep.name do
let deps ← pkg.depConfigs.mapM fun dep => fetchOrCreate dep.name do
if let some entry := (← getThe (NameMap PackageEntry)).find? dep.name then
entry.materialize dep ws.dir ws.relPkgsDir ws.lakeEnv.pkgUrlMap
else
@ -145,7 +188,7 @@ def Workspace.updateAndMaterialize (ws : Workspace)
return pkg
else
-- Load the package
let depPkg ← dep.loadPackage ws.dir ws.lakeEnv pkg.leanOpts reconfigure
let depPkg ← liftM <| loadDepPackage dep leanOpts reconfigure
if depPkg.name ≠ dep.name then
logWarning s!"{pkg.name}: package '{depPkg.name}' was required as '{dep.name}'"
-- Materialize locked dependencies
@ -162,46 +205,47 @@ def Workspace.updateAndMaterialize (ws : Workspace)
modifyThe (NameMap Package) (·.insert dep.name depPkg)
return depPkg
-- Resolve dependencies's dependencies recursively
return {pkg with opaqueDeps := ← deps.mapM (.mk <$> resolve ·)}
match res with
| (.ok root, deps) =>
let ws : Workspace ← {ws with root}.finalize
let manifest : Manifest := {
name := ws.root.name
lakeDir := ws.relLakeDir
packagesDir? := ws.relPkgsDir
}
let manifest := ws.packages.foldl (init := manifest) fun manifest pkg =>
match deps.find? pkg.name with
| some dep => manifest.addPackage <|
dep.manifestEntry.setManifestFile pkg.relManifestFile
| none => manifest -- should only be the case for the root
manifest.saveToFile ws.manifestFile
LakeT.run ⟨ws⟩ <| ws.packages.forM fun pkg => do
unless pkg.postUpdateHooks.isEmpty do
logInfo s!"{pkg.name}: running post-update hooks"
pkg.postUpdateHooks.forM fun hook => hook.get.fn pkg
return ws
| (.error cycle, _) =>
let cycle := cycle.map (s!" {·}")
error s!"dependency cycle detected:\n{"\n".intercalate cycle}"
let pkg := {pkg with opaqueDeps := ← deps.mapM (.mk <$> resolve ·)}
modifyThe Workspace (·.addPackage pkg)
return pkg
let ws : Workspace := {ws with root}
let manifest : Manifest := {
name := ws.root.name
lakeDir := ws.relLakeDir
packagesDir? := ws.relPkgsDir
}
let manifest := ws.packages.foldl (init := manifest) fun manifest pkg =>
match deps.find? pkg.name with
| some dep => manifest.addPackage <|
dep.manifestEntry.setManifestFile pkg.relManifestFile |>.setConfigFile pkg.relConfigFile
| none => manifest -- should only be the case for the root
manifest.saveToFile ws.manifestFile
LakeT.run ⟨ws⟩ <| ws.packages.forM fun pkg => do
unless pkg.postUpdateHooks.isEmpty do
logInfo s!"{pkg.name}: running post-update hooks"
pkg.postUpdateHooks.forM fun hook => hook.get.fn pkg
return ws
/--
Resolving a workspace's dependencies using a manifest,
downloading and/or updating them as necessary.
-/
def Workspace.materializeDeps (ws : Workspace) (manifest : Manifest) (reconfigure := false) : LogIO Workspace := do
if !manifest.packages.isEmpty && manifest.packagesDir? != some (normalizePath ws.relPkgsDir) then
def Workspace.materializeDeps
(ws : Workspace) (manifest : Manifest)
(leanOpts : Options := {}) (reconfigure := false)
: LogIO Workspace := do
if !manifest.packages.isEmpty && manifest.packagesDir? != some (mkRelPathString ws.relPkgsDir) then
logWarning <|
"manifest out of date: packages directory changed; " ++
"use `lake update` to rebuild the manifest (warning: this will update ALL workspace dependencies)"
let relPkgsDir := manifest.packagesDir?.getD ws.relPkgsDir
let pkgEntries := manifest.packages.foldl (init := mkNameMap PackageEntry)
fun map entry => map.insert entry.name entry
let res ← EStateT.run' (mkNameMap Package) do
buildAcyclic (·.name) ws.root fun pkg resolve => do
let topLevel := pkg.name = ws.root.name
let deps ← IO.ofExcept <| loadDepsFromEnv pkg.configEnv pkg.leanOpts
let rootPkg := ws.root
let (root, ws) ← StateT.run (s := ws) <| StateT.run' (s := mkNameMap Package) do
resolveDepsAcyclic rootPkg fun pkg resolve => do
let topLevel := pkg.name = rootPkg.name
let deps := pkg.depConfigs
if topLevel then
if manifest.packages.isEmpty && !deps.isEmpty then
error "missing manifest; use `lake update` to generate one"
@ -219,8 +263,9 @@ def Workspace.materializeDeps (ws : Workspace) (manifest : Manifest) (reconfigur
| _, _ => warnOutOfDate "source kind (git/path)"
let depPkgs ← deps.mapM fun dep => fetchOrCreate dep.name do
if let some entry := pkgEntries.find? dep.name then
let ws ← getThe Workspace
let result ← entry.materialize dep ws.dir relPkgsDir ws.lakeEnv.pkgUrlMap
result.loadPackage ws.dir ws.lakeEnv pkg.leanOpts reconfigure
liftM <| loadDepPackage result leanOpts reconfigure
else if topLevel then
error <|
s!"dependency '{dep.name}' not in manifest; " ++
@ -230,13 +275,10 @@ def Workspace.materializeDeps (ws : Workspace) (manifest : Manifest) (reconfigur
s!"dependency '{dep.name}' of '{pkg.name}' not in manifest; " ++
"this suggests that the manifest is corrupt;" ++
"use `lake update` to generate a new, complete file (warning: this will update ALL workspace dependencies)"
return {pkg with opaqueDeps := ← depPkgs.mapM (.mk <$> resolve ·)}
match res with
| Except.ok root =>
({ws with root}).finalize
| Except.error cycle =>
let cycle := cycle.map (s!" {·}")
error s!"dependency cycle detected:\n{"\n".intercalate cycle}"
let pkg := {pkg with opaqueDeps := ← depPkgs.mapM (.mk <$> resolve ·)}
modifyThe Workspace (·.addPackage pkg)
return pkg
return {ws with root}
/--
Load a `Workspace` for a Lake package by
@ -245,16 +287,18 @@ If `updateDeps` is true, updates the manifest before resolving dependencies.
-/
def loadWorkspace (config : LoadConfig) (updateDeps := false) : LogIO Workspace := do
let rc := config.reconfigure
let leanOpts := config.leanOpts
let ws ← loadWorkspaceRoot config
if updateDeps then
ws.updateAndMaterialize {} rc
ws.updateAndMaterialize leanOpts {} rc
else if let some manifest ← Manifest.load? ws.manifestFile then
ws.materializeDeps manifest rc
ws.materializeDeps manifest leanOpts rc
else
ws.updateAndMaterialize {} rc
ws.updateAndMaterialize leanOpts {} rc
/-- Updates the manifest for the loaded Lake workspace (see `updateAndMaterialize`). -/
def updateManifest (config : LoadConfig) (toUpdate : NameSet := {}) : LogIO Unit := do
let rc := config.reconfigure
let leanOpts := config.leanOpts
let ws ← loadWorkspaceRoot config
discard <| ws.updateAndMaterialize toUpdate rc
discard <| ws.updateAndMaterialize leanOpts toUpdate rc

21
src/lake/Lake/Load/Manifest.lean
View file

@ -5,6 +5,7 @@ Authors: Mac Malone, Gabriel Ebner
-/
import Lake.Util.Log
import Lake.Util.Name
import Lake.Util.FilePath
import Lake.Load.Config
import Lake.Config.Workspace
@ -27,20 +28,6 @@ inductive PackageEntryV6
(inputRev? : Option String) (subDir? : Option FilePath)
deriving FromJson, ToJson, Inhabited
/-- Set `/` as the path separator, even on Windows. -/
def normalizePath (path : FilePath) : FilePath :=
if System.Platform.isWindows then
path.toString.map fun c => if c = '\\' then '/' else c
else
path.toString
/--
Use `/` and instead of `\\` in file paths
when serializing the manifest on Windows.
-/
local instance : ToJson FilePath where
toJson path := toJson <| normalizePath path
/-- An entry for a package stored in the manifest. -/
inductive PackageEntry
/--
@ -142,6 +129,12 @@ def setInherited : PackageEntry → PackageEntry
@[inline] protected def manifestFile? : PackageEntry → Option FilePath
| .path (manifestFile? := manifestFile?) .. | .git (manifestFile? := manifestFile?) .. => manifestFile?
def setConfigFile (path : FilePath) : PackageEntry → PackageEntry
| .path name inherited _ manifestFile? dir =>
.path name inherited path manifestFile? dir
| .git name inherited _ manifestFile? url rev inputRev? subDir? =>
.git name inherited path manifestFile? url rev inputRev? subDir?
def setManifestFile (path? : Option FilePath) : PackageEntry → PackageEntry
| .path name inherited configFile _ dir =>
.path name inherited configFile path? dir

18
src/lake/Lake/Load/Package.lean
View file

@ -61,12 +61,13 @@ def PackageConfig.loadFromEnv
evalConstCheck env opts _ ``PackageConfig declName
/--
Load the remainder of a `Package`
from its configuration environment after resolving its dependencies.
Load the optional elements of a `Package` from the Lean environment.
This is done after loading its core configuration but before resolving
its dependencies.
-/
def Package.finalize (self : Package) (deps : Array Package) : LogIO Package := do
let env := self.configEnv
let opts := self.leanOpts
def Package.loadFromEnv
(self : Package) (env : Environment) (opts : Options)
: LogIO Package := do
let strName := self.name.toString (escape := false)
-- Load Script, Facet, Target, and Hook Configurations
@ -106,6 +107,8 @@ def Package.finalize (self : Package) (deps : Array Package) : LogIO Package :=
else
error s!"post-update hook was defined in `{decl.pkg}`, but was registered in `{self.name}`"
| .error e => error e
let depConfigs ← IO.ofExcept <| packageDepAttr.getAllEntries env |>.mapM fun name =>
evalConstCheck env opts Dependency ``Dependency name
-- Deprecation warnings
unless self.config.manifestFile.isNone do
@ -115,9 +118,8 @@ def Package.finalize (self : Package) (deps : Array Package) : LogIO Package :=
-- Fill in the Package
return {self with
opaqueDeps := deps.map (.mk ·)
leanLibConfigs, leanExeConfigs, externLibConfigs
opaqueTargetConfigs, defaultTargets, scripts, defaultScripts,
depConfigs, leanLibConfigs, leanExeConfigs, externLibConfigs
opaqueTargetConfigs, defaultTargets, scripts, defaultScripts
postUpdateHooks
}

276
src/lake/Lake/Load/Toml.lean Normal file
View file

@ -0,0 +1,276 @@
/-
Copyright (c) 2024 Mac Malone. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Mac Malone
-/
import Lake.Toml.Load
import Lake.Toml.Decode
import Lake.Config.Package
import Lake.Util.Log
open Lean Parser
/-! # TOML Loader
Load a package from a TOML Lake configuration file.
-/
namespace Lake
open Toml
/-! ## Data Decoders -/
def takeNamePart (ss : Substring) (pre : Name) : (Substring × Name) :=
if ss.isEmpty then
(ss, .anonymous)
else
let curr := ss.front
if isIdBeginEscape curr then
let ss := ss.drop 1
let startPos := ss.startPos
let ss := ss.dropWhile (!isIdEndEscape ·)
if isIdEndEscape ss.front then
let id := ss.str.extract startPos ss.startPos
(ss, Name.str pre id)
else
(ss, .anonymous)
else if isIdFirst curr then
let startPos := ss.startPos
let ss := ss.drop 1 |>.dropWhile isIdRest
let id := ss.str.extract startPos ss.startPos
(ss, Name.str pre id)
else if curr.isDigit then
let startPos := ss.startPos
let ss := ss.drop 1 |>.dropWhile Char.isDigit
let digits := ss.str.extract startPos ss.startPos
let n := (Syntax.decodeNatLitVal? digits).get!
(ss, Name.num pre n)
else
(ss, .anonymous)
partial def takeName (ss : Substring) : (Substring × Name) :=
let rec takeRest ss pre :=
if ss.front == '.' then
let startPos := ss.startPos
let (ss, n) := takeNamePart (ss.drop 1) pre
if n.isAnonymous then ({ss with startPos}, pre) else takeRest ss n
else
(ss, pre)
let (ss, n) := takeNamePart ss .anonymous
if n.isAnonymous then (ss, .anonymous) else takeRest ss n
def Glob.ofString? (v : String) : Option Glob := do
let (ss, n) := takeName v.toSubstring
if n.isAnonymous then failure
if h : ss.str.atEnd ss.startPos then
return .one n
else if ss.str.get' ss.startPos h == '.' then
match (ss.drop 1).front with
| '+' => return .submodules n
| '*' => return .andSubmodules n
| _ => failure
else
failure
protected def Glob.decodeToml (v : Value) : Except DecodeError Glob := do
match inline <| Glob.ofString? (← v.decodeString) with
| some v => return v
| none => throw <| .mk v.ref "expected glob"
instance : DecodeToml Glob := ⟨(Glob.decodeToml ·)⟩
protected def LeanOptionValue.decodeToml : Value → Except DecodeError LeanOptionValue
| .string _ v => return .ofString v
| .boolean _ v => return .ofBool v
| .integer _ (.ofNat v) => return .ofNat v
| x => throw (.mk x.ref "expected string, boolean, or nonnegative integer")
instance : DecodeToml LeanOptionValue := ⟨(LeanOptionValue.decodeToml ·)⟩
protected def LeanOption.decodeToml (v : Value) : Except (Array DecodeError) LeanOption := do
match v with
| .array ref vs =>
if h : vs.size = 2 then ensureDecode do
let name : Name ← tryDecode <| decodeToml vs[0]
let value ← tryDecode <| decodeToml vs[1]
return {name, value}
else
throw #[.mk ref "expected array of size 2"]
| .table ref t => ensureDecode do
let name ← t.tryDecode `name ref
let value ← t.tryDecode `value ref
return {name, value}
| v =>
throw #[.mk v.ref "expected array or table"]
instance : DecodeToml LeanOption := ⟨LeanOption.decodeToml⟩
protected def BuildType.decodeToml (v : Value) : Except DecodeError BuildType := do
match inline <| BuildType.ofString? (← v.decodeString) with
| some v => return v
| none => throw <| .mk v.ref "expected one of 'debug', 'relWithDebInfo', 'minSizeRel', 'release'"
instance : DecodeToml BuildType := ⟨(BuildType.decodeToml ·)⟩
protected def Backend.decodeToml (v : Value) : Except DecodeError Backend := do
match inline <| Backend.ofString? (← v.decodeString) with
| some v => return v
| none => throw <| .mk v.ref "expected one of 'c', 'llvm', or 'default'"
instance : DecodeToml Backend := ⟨(Backend.decodeToml ·)⟩
partial def decodeLeanOptionsAux
(v : Value) (k : Name) (vs : Except (Array DecodeError) (Array LeanOption))
: Except (Array DecodeError) (Array LeanOption) :=
match v with
| .table _ t => t.items.foldl (init := vs) fun vs (k',v) =>
decodeLeanOptionsAux v (k ++ k') vs
| v => mergeErrors vs (decodeToml v) fun vs v => vs.push ⟨k,v⟩
def decodeLeanOptions (v : Value) : Except (Array DecodeError) (Array LeanOption) :=
match v with
| .array _ vs => decodeArray vs
| .table _ t => t.items.foldl (init := .ok #[]) fun vs (k,v) => decodeLeanOptionsAux v k vs
| v =>
throw #[.mk v.ref "expected array or table"]
/-! ## Configuration Decoders -/
protected def WorkspaceConfig.decodeToml (t : Table) : Except (Array DecodeError) WorkspaceConfig := ensureDecode do
let packagesDir ← t.tryDecodeD `packagesDir defaultPackagesDir
return {packagesDir}
instance : DecodeToml WorkspaceConfig := ⟨fun v => do WorkspaceConfig.decodeToml (← v.decodeTable)⟩
protected def LeanConfig.decodeToml (t : Table) : Except (Array DecodeError) LeanConfig := ensureDecode do
let buildType ← t.tryDecodeD `buildType .release
let backend ← t.tryDecodeD `backend .default
let platformIndependent ← t.tryDecode? `platformIndependent
let leanOptions ← optDecodeD #[] (t.find? `leanOptions) decodeLeanOptions
let moreServerOptions ← optDecodeD #[] (t.find? `moreServerOptions) decodeLeanOptions
let moreLeanArgs ← t.tryDecodeD `moreLeanArgs #[]
let weakLeanArgs ← t.tryDecodeD `weakLeanArgs #[]
let moreLeancArgs ← t.tryDecodeD `moreLeancArgs #[]
let weakLeancArgs ← t.tryDecodeD `weakLeancArgs #[]
let moreLinkArgs ← t.tryDecodeD `moreLinkArgs #[]
let weakLinkArgs ← t.tryDecodeD `weakLinkArgs #[]
return {
buildType, backend, platformIndependent, leanOptions, moreServerOptions,
moreLeanArgs, weakLeanArgs, moreLeancArgs, weakLeancArgs, moreLinkArgs, weakLinkArgs
}
instance : DecodeToml LeanConfig := ⟨fun v => do LeanConfig.decodeToml (← v.decodeTable)⟩
protected def PackageConfig.decodeToml (t : Table) (ref := Syntax.missing) : Except (Array DecodeError) PackageConfig := ensureDecode do
let name ← stringToLegalOrSimpleName <$> t.tryDecode `name ref
let precompileModules ← t.tryDecodeD `precompileModules false
let moreGlobalServerArgs ← t.tryDecodeD `moreGlobalServerArgs #[]
let srcDir ← t.tryDecodeD `srcDir "."
let buildDir ← t.tryDecodeD `buildDir defaultBuildDir
let leanLibDir ← t.tryDecodeD `leanLibDir defaultLeanLibDir
let nativeLibDir ← t.tryDecodeD `nativeLibDir defaultNativeLibDir
let binDir ← t.tryDecodeD `binDir defaultBinDir
let irDir ← t.tryDecodeD `irDir defaultIrDir
let releaseRepo ← t.tryDecode? `releaseRepo
let buildArchive? ← t.tryDecode? `buildArchive
let preferReleaseBuild ← t.tryDecodeD `preferReleaseBuild false
let toLeanConfig ← tryDecode <| LeanConfig.decodeToml t
let toWorkspaceConfig ← tryDecode <| WorkspaceConfig.decodeToml t
return {
name, precompileModules, moreGlobalServerArgs,
srcDir, buildDir, leanLibDir, nativeLibDir, binDir, irDir,
releaseRepo, buildArchive?, preferReleaseBuild
toLeanConfig, toWorkspaceConfig
}
instance : DecodeToml PackageConfig := ⟨fun v => do PackageConfig.decodeToml (← v.decodeTable) v.ref⟩
protected def LeanLibConfig.decodeToml (t : Table) (ref := Syntax.missing) : Except (Array DecodeError) LeanLibConfig := ensureDecode do
let name : Name ← t.tryDecode `name ref
let srcDir ← t.tryDecodeD `srcDir "."
let roots ← t.tryDecodeD `roots #[name]
let globs ← optDecodeD (roots.map Glob.one) (t.find? `globs) (·.decodeArrayOrSingleton)
let libName ← t.tryDecodeD `libName (name.toString (escape := false))
let precompileModules ← t.tryDecodeD `precompileModules false
let defaultFacets ← t.tryDecodeD `defaultFacets #[LeanLib.leanArtsFacet]
let toLeanConfig ← tryDecode <| LeanConfig.decodeToml t
return {
name, srcDir, roots, globs, libName,
precompileModules, defaultFacets, toLeanConfig
}
instance : DecodeToml LeanLibConfig := ⟨fun v => do LeanLibConfig.decodeToml (← v.decodeTable) v.ref⟩
protected def LeanExeConfig.decodeToml (t : Table) (ref := Syntax.missing) : Except (Array DecodeError) LeanExeConfig := ensureDecode do
let name ← stringToLegalOrSimpleName <$> t.tryDecode `name ref
let srcDir ← t.tryDecodeD `srcDir "."
let root ← t.tryDecodeD `root name
let exeName ← t.tryDecodeD `exeName (name.toStringWithSep "-" (escape := false))
let supportInterpreter ← t.tryDecodeD `supportInterpreter false
let toLeanConfig ← tryDecode <| LeanConfig.decodeToml t
return {name, srcDir, root, exeName, supportInterpreter, toLeanConfig}
instance : DecodeToml LeanExeConfig := ⟨fun v => do LeanExeConfig.decodeToml (← v.decodeTable) v.ref⟩
protected def Source.decodeToml (t : Table) (ref := Syntax.missing) : Except (Array DecodeError) Source := do
let typeVal ← t.decodeValue `type
match (← typeVal.decodeString) with
| "path" =>
return Source.path (← t.decode `dir)
| "git" => ensureDecode do
return Source.git (← t.tryDecode `url ref) (← t.tryDecode? `rev) (← t.tryDecode? `subDir)
| _ =>
throw #[DecodeError.mk typeVal.ref "expected one of 'path' or 'git'"]
instance : DecodeToml Source := ⟨fun v => do Source.decodeToml (← v.decodeTable) v.ref⟩
protected def Dependency.decodeToml (t : Table) (ref := Syntax.missing) : Except (Array DecodeError) Dependency := ensureDecode do
let name ← t.tryDecode `name ref
let src ← id do
if let some dir ← t.tryDecode? `path then
return Source.path dir
else if let some g := t.find? `git then
match g with
| .string _ url =>
return Source.git url (← t.tryDecode? `rev) (← t.tryDecode? `subDir)
| .table ref t =>
return Source.git (← t.tryDecode `url ref) (← t.tryDecode? `rev) (← t.tryDecode? `subDir)
| _ =>
modify (·.push <| .mk g.ref "expected string or table")
return default
else
t.tryDecode `source ref
let opts ← t.tryDecodeD `options {}
return {name, src, opts}
instance : DecodeToml Dependency := ⟨fun v => do Dependency.decodeToml (← v.decodeTable) v.ref⟩
/-! ## Root Loader -/
def loadTomlConfig (dir relDir relConfigFile : FilePath) : LogIO Package := do
let configFile := dir / relConfigFile
let input ← IO.FS.readFile configFile
let ictx := mkInputContext input relConfigFile.toString
match (← loadToml ictx |>.toBaseIO) with
| .ok table =>
let (pkg, errs) := Id.run <| StateT.run (s := (#[] : Array DecodeError)) do
let config ← tryDecode <| PackageConfig.decodeToml table
let leanLibConfigs ← mkRBArray (·.name) <$> table.tryDecodeD `lean_lib #[]
let leanExeConfigs ← mkRBArray (·.name) <$> table.tryDecodeD `lean_exe #[]
let defaultTargets ← table.tryDecodeD `defaultTargets #[]
let depConfigs ← table.tryDecodeD `require #[]
return {
dir, relDir, relConfigFile,
config, depConfigs, leanLibConfigs, leanExeConfigs, defaultTargets
}
if errs.isEmpty then
return pkg
else
errs.forM fun {ref, msg} =>
let pos := ictx.fileMap.toPosition <| ref.getPos?.getD 0
logError <| mkErrorStringWithPos ictx.fileName pos msg
failure
| .error log =>
log.forM fun msg => do logError (← msg.toString)
failure

6
src/lake/Lake/Toml.lean Normal file
View file

@ -0,0 +1,6 @@
/-
Copyright (c) 2024 Mac Malone. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Mac Malone
-/
import Lake.Toml.Load

10
src/lake/Lake/Toml/Data.lean Normal file
View file

@ -0,0 +1,10 @@
/-
Copyright (c) 2024 Mac Malone. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Mac Malone
-/
import Lake.Toml.Data.Value
/-!
# TOML Data Types
-/

184
src/lake/Lake/Toml/Data/DateTime.lean Normal file
View file

@ -0,0 +1,184 @@
/-
Copyright (c) 2024 Mac Malone. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Mac Malone
-/
/-!
# TOML Date-Time
Defines data types for representing a TOML [date-time][1].
TOML date-times are based on [IETF RFC 3339][2] with some components
optionally left out, creating four distinct variants.
* **Offset Date-Time**: A full RFC 3339 date-time.
* **Local Date-Time**: An RFC 3339 date-time without the time zone.
* **Local Date**: The date portion of an RFC 3339 date-time (year-month-day).
* **Local Time**: The time portion of an RFC 3339 date-time (without time zone).
[1]: https://toml.io/en/v1.0.0#offset-date-time
[2]: https://datatracker.ietf.org/doc/html/rfc3339
-/
namespace Lake.Toml
def lpad (s : String) (c : Char) (len : Nat) : String :=
"".pushn c (len - s.length) ++ s
def rpad (s : String) (c : Char) (len : Nat) : String :=
s.pushn c (len - s.length)
def zpad (n : Nat) (len : Nat) : String :=
lpad (toString n) '0' len
/-- A TOML date (year-month-day). -/
structure Date where
year : Nat
month : Nat
day : Nat
deriving Inhabited, DecidableEq, Ord
namespace Date
abbrev IsLeapYear (y : Nat) : Prop :=
y % 4 = 0 ∧ (y % 100 ≠ 0 ∨ y % 400 = 0)
abbrev IsValidMonth (m : Nat) : Prop :=
m ≥ 1 ∧ m ≤ 12
def maxDay (y m : Nat) : Nat :=
if m = 2 then
if IsLeapYear y then 29 else 28
else if m ≤ 7 then
30 + (m % 2)
else
31 - (m % 2)
abbrev IsValidDay (y m d : Nat) : Prop :=
d ≥ 1 ∧ d ≤ maxDay y m
def ofValid? (year month day : Nat) : Option Date := do
guard (IsValidMonth month ∧ IsValidDay year month day)
return {year, month, day}
def ofString? (t : String) : Option Date := do
match t.split (· == '-') with
| [y,m,d] =>
ofValid? (← y.toNat?) (← m.toNat?) (← d.toNat?)
| _ => none
protected def toString (d : Date) : String :=
s!"{zpad d.year 4}-{zpad d.month 2}-{zpad d.day 2}"
instance : ToString Date := ⟨Date.toString⟩
end Date
/--
A TOML time (hour:minute:second.fraction).
We do not represent whole time as seconds to due to the possibility
of leap seconds in RFC 3339 times.
-/
structure Time where
hour : Nat
minute : Nat
second : Nat
fracExponent : Nat := 0
fracMantissa : Nat := 0
deriving Inhabited, DecidableEq
namespace Time
abbrev IsValidHour (h : Nat) : Prop :=
h ≤ 23
abbrev IsValidMinute (m : Nat) : Prop :=
m ≤ 59
abbrev IsValidSecond (s : Nat) : Prop :=
s ≤ 60
def zero : Time :=
{hour := 0, minute := 0, second := 0}
instance : OfNat Time (nat_lit 0) := ⟨Time.zero⟩
def ofValid? (hour minute second : Nat) : Option Time := do
guard (IsValidHour hour ∧ IsValidMinute minute ∧ IsValidSecond second)
return {hour, minute, second}
def ofString? (t : String) : Option Time := do
match t.split (· == ':') with
| [h,m,s] =>
match s.split (· == '.') with
| [s,f] =>
let time ← ofValid? (← h.toNat?) (← m.toNat?) (← s.toNat?)
return {time with fracExponent := f.length-1, fracMantissa := ← f.toNat?}
| [s] =>
ofValid? (← h.toNat?) (← m.toNat?) (← s.toNat?)
| _ => none
| [h,m] =>
ofValid? (← h.toNat?) (← m.toNat?) 0
| _ => none
protected def toString (t : Time) : String :=
let s := s!"{zpad t.hour 2}:{zpad t.minute 2}:{zpad t.second 2}"
if t.fracMantissa = 0 then
s
else
s!"{s}.{rpad (zpad t.fracMantissa t.fracExponent) '0' 3}"
instance : ToString Time := ⟨Time.toString⟩
end Time
/-- A TOML date-time. -/
inductive DateTime
| offsetDateTime (date : Date) (time : Time) (offset? : Option (Bool × Time) := none)
| localDateTime (date : Date) (time : Time)
| localDate (date : Date)
| localTime (time : Time)
deriving Inhabited, DecidableEq
instance : Coe Date DateTime := ⟨DateTime.localDate⟩
instance : Coe Time DateTime := ⟨DateTime.localTime⟩
namespace DateTime
def ofString? (dt : String) : Option DateTime := do
match dt.split (fun c => c == 'T' || c == 't' || c == ' ') with
| [d,t] =>
let d ← Date.ofString? d
if t.back == 'Z' || t.back == 'z' then
return offsetDateTime d (← Time.ofString? <| t.dropRight 1)
else if let [t,o] := t.split (· == '+') then
return offsetDateTime d (← Time.ofString? t) (false, ← Time.ofString? o)
else if let [t,o] := t.split (· == '-') then
return offsetDateTime d (← Time.ofString? t) (true, ← Time.ofString? o)
else
return localDateTime d (← Time.ofString? t)
| [x] =>
if x.any (· == ':') then
return localTime (← Time.ofString? x)
else
return localDate (← Date.ofString? x)
| _ => none
protected def toString (dt : DateTime) : String :=
match dt with
| .offsetDateTime d t o? =>
if let some (s,o) := o? then
if s then
s!"{d}T{t}-{zpad o.hour 2}:{zpad o.minute 2}"
else
s!"{d}T{t}+{zpad o.hour 2}:{zpad o.minute 2}"
else
s!"{d}T{t}Z"
| .localDateTime d t => s!"{d}T{t}"
| .localDate d => d.toString
| .localTime t => t.toString
instance : ToString DateTime := ⟨DateTime.toString⟩
end DateTime

118
src/lake/Lake/Toml/Data/Dict.lean Normal file
View file

@ -0,0 +1,118 @@
/-
Copyright (c) 2024 Mac Malone. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Mac Malone
-/
import Lean.Data.NameMap
/-! # Red-Black Dictionary
Defines an **insertion-ordered** key-value mapping backed by an red-black tree.
Implemented via a key-index `RBMap` into an `Array` of key-value pairs.
-/
open Lean
namespace Lake.Toml
/- An insertion-ordered key-value mapping backed by a red-black tree. -/
structure RBDict (α : Type u) (β : Type v) (cmp : α → α → Ordering) where
items : Array (α × β)
indices : RBMap α Nat cmp
deriving Inhabited
abbrev NameDict (α : Type u) := RBDict Name α Name.quickCmp
namespace RBDict
def empty : RBDict α β cmp :=
{items := #[], indices := {}}
instance : EmptyCollection (RBDict α β cmp) := ⟨RBDict.empty⟩
def mkEmpty (capacity : Nat) : RBDict α β cmp :=
{items := .mkEmpty capacity, indices := {}}
def ofArray (items : Array (α × β)) : RBDict α β cmp := Id.run do
let mut indices := mkRBMap α Nat cmp
for h : i in [0:items.size] do
indices := indices.insert (items[i]'h.upper).1 i
return {items, indices}
protected def beq [BEq (α × β)] (self other : RBDict α β cmp) : Bool :=
self.items == other.items
instance [BEq (α × β)] : BEq (RBDict α β cmp) := ⟨RBDict.beq⟩
abbrev size (t : RBDict α β cmp) : Nat :=
t.items.size
abbrev isEmpty (t : RBDict α β cmp) : Bool :=
t.items.isEmpty
def keys (t : RBDict α β cmp) : Array α :=
t.items.map (·.1)
def values (t : RBDict α β cmp) : Array β :=
t.items.map (·.2)
def contains (k : α) (t : RBDict α β cmp) : Bool :=
t.indices.contains k
def findIdx? (k : α) (t : RBDict α β cmp) : Option (Fin t.size) := do
let i ← t.indices.find? k; if h : i < t.items.size then some ⟨i, h⟩ else none
def findEntry? (k : α) (t : RBDict α β cmp) : Option (α × β) := do
return t.items[← t.findIdx? k]
@[inline] def find? (k : α) (t : RBDict α β cmp) : Option β := do
return (← t.findEntry? k).2
def push (k : α) (v : β) (t : RBDict α β cmp) : RBDict α β cmp :=
{items := t.items.push ⟨k,v⟩, indices := t.indices.insert k t.items.size}
@[specialize] def alter (k : α) (f : Option β → β) (t : RBDict α β cmp) : RBDict α β cmp :=
if let some i := t.findIdx? k then
{t with items := t.items.modify i fun (k, v) => (k, f (some v))}
else
t.push k (f none)
def insert (k : α) (v : β) (t : RBDict α β cmp) : RBDict α β cmp :=
if let some i := t.findIdx? k then
if h : i < t.items.size then
{t with items := t.items.set ⟨i,h⟩ (k,v)}
else
t.push k v
else
t.push k v
/-- Inserts the value into the dictionary if `p` is `true`. -/
@[macro_inline] def insertIf (p : Bool) (k : α) (v : β) (t : RBDict α β cmp) : RBDict α β cmp :=
if p then t.insert k v else t
/-- Inserts the value into the dictionary if `p` is `false`. -/
@[macro_inline] def insertUnless (p : Bool) (k : α) (v : β) (t : RBDict α β cmp) : RBDict α β cmp :=
if p then t else t.insert k v
/-- Insert the value into the dictionary if it is not `none`. -/
@[macro_inline] def insertSome (k : α) (v? : Option β) (t : RBDict α β cmp) : RBDict α β cmp :=
if let some v := v? then t.insert k v else t
def appendArray (self : RBDict α β cmp) (other : Array (α × β)): RBDict α β cmp :=
other.foldl (fun t (k,v) => t.insert k v) self
instance : HAppend (RBDict α β cmp) (Array (α × β)) (RBDict α β cmp) := ⟨RBDict.appendArray⟩
@[inline] def append (self other : RBDict α β cmp) : RBDict α β cmp :=
self.appendArray other.items
instance : Append (RBDict α β cmp) := ⟨RBDict.append⟩
@[inline] def map (f : α → β → γ) (t : RBDict α β cmp) : RBDict α γ cmp :=
{t with items := t.items.map fun ⟨k, v⟩ => ⟨k, f k v⟩}
@[inline] def filter (p : α → β → Bool) (t : RBDict α β cmp) : RBDict α β cmp :=
t.items.foldl (init := {}) fun t (k, v) => if p k v then t.push k v else t
@[inline] def filterMap (f : α → β → Option γ) (t : RBDict α β cmp) : RBDict α γ cmp :=
t.items.foldl (init := {}) fun t ⟨k, v⟩ => if let some v := f k v then t.push k v else t

125
src/lake/Lake/Toml/Data/Value.lean Normal file
View file

@ -0,0 +1,125 @@
/-
Copyright (c) 2024 Mac Malone. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Mac Malone
-/
import Lake.Toml.Data.Dict
import Lake.Toml.Data.DateTime
/-!
# TOML Value
-/
open Lean
namespace Lake.Toml
/-- A TOML value with optional source info. -/
inductive Value
| string (ref : Syntax) (s : String)
| integer (ref : Syntax) (n : Int)
| float (ref : Syntax) (n : Float)
| boolean (ref : Syntax) (b : Bool)
| dateTime (ref : Syntax) (dt : DateTime)
| array (ref : Syntax) (xs : Array Value)
| private table' (ref : Syntax) (xs : RBDict Name Value Name.quickCmp)
deriving Inhabited, BEq
/-- A TOML table, an ordered key-value map of TOML values (`Lake.Toml.Value`). -/
abbrev Table := NameDict Value
@[inline] def Table.empty : Table := RBDict.empty
@[inline] def Table.mkEmpty (capacity : Nat) : Table := RBDict.mkEmpty capacity
@[match_pattern] abbrev Value.table (ref : Syntax) (t : Table) :=
Value.table' ref t
@[inline] def Value.ref : Value → Syntax
| .string (ref := ref) .. => ref
| .integer (ref := ref) .. => ref
| .float (ref := ref) .. => ref
| .boolean (ref := ref) .. => ref
| .dateTime (ref := ref) .. => ref
| .array (ref := ref) .. => ref
| .table (ref := ref) .. => ref
--------------------------------------------------------------------------------
/-! ## Pretty Printing -/
--------------------------------------------------------------------------------
def ppString (s : String) : String :=
let s := s.foldl (init := "\"") fun s c =>
match c with
| '\x08' => s ++ "\\b"
| '\t' => s ++ "\\t"
| '\n' => s ++ "\\n"
| '\x0C' => s ++ "\\f"
| '\r' => s ++ "\\r"
| '\"' => s ++ "\\\""
| '\\' => s ++ "\\\\"
| _ =>
if c.val < 0x20 || c.val == 0x7F then
s ++ "\\u" ++ lpad (String.mk <| Nat.toDigits 16 c.val.toNat) '0' 4
else
s.push c
s.push '\"'
def ppSimpleKey (k : String) : String :=
if k.all (fun c => c.isAlphanum || c == '_' || c == '-') then
k
else
ppString k
partial def ppKey (k : Name) : String :=
match k with
| .str p s =>
if p.isAnonymous then
ppSimpleKey s
else
s!"{ppKey p}.{ppSimpleKey s}"
| _ => ""
mutual
partial def ppInlineTable (t : Table) : String :=
let xs := t.items.map fun (k,v) => s!"{ppKey k} = {Value.toString v}"
"{" ++ ", ".intercalate xs.toList ++ "}"
partial def ppInlineArray (vs : Array Value) : String :=
let xs := vs.map Value.toString
"[" ++ ", ".intercalate xs.toList ++ "]"
partial def Value.toString (v : Value) : String :=
match v with
| .string _ s => ppString s
| .integer _ n => toString n
| .float _ n => toString n
| .boolean _ b => toString b
| .dateTime _ dt => toString dt
| .array _ vs => ppInlineArray vs
| .table _ t => ppInlineTable t
end
instance : ToString Value := ⟨Value.toString⟩
def ppTable (t : Table) : String :=
String.trimLeft <| t.items.foldl (init := "") fun s (k,v) =>
match v with
| .array _ vs =>
if vs.all (· matches .table ..) then
vs.foldl (init := s) fun s v =>
match v with
| .table _ t =>
let s := s ++ s!"\n[[{ppKey k}]]\n"
t.items.foldl (fun s (k,v) => appendKeyval s k v) s
| _ => unreachable!
else
s.append s!"{ppKey k} = {ppInlineArray vs}\n"
| .table _ t =>
let s := s ++ s!"\n[{ppKey k}]\n"
t.items.foldl (fun s (k,v) => appendKeyval s k v) s
| _ => appendKeyval s k v
where
appendKeyval s k v :=
s.append s!"{ppKey k} = {v}\n"

188
src/lake/Lake/Toml/Decode.lean Normal file
View file

@ -0,0 +1,188 @@
/-
Copyright (c) 2024 Mac Malone. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Mac Malone
-/
import Lake.Toml.Data
/-!
# TOML Decoders
This module contains definitions to assist in decoding TOML data values
into concrete user types.
-/
namespace Lake
open Lean Toml
/-!
## Generic Decode Helpers
-/
instance : MonadLift (Except ε) (Except (Array ε)) where
monadLift x := x.mapError Array.singleton
/-- Run the decode action. If there were errors, throw. Otherwise, return the result. -/
@[inline] def ensureDecode (x : StateM (Array ε) α) : Except (Array ε) α :=
let (a, es) := x.run Array.empty; if es.isEmpty then pure a else throw es
/-- Run the decode action. If it fails, add the errors to the state and return `default`. -/
@[inline] def tryDecodeD (default : α) (x : Except (Array ε) α) : StateM (Array ε) α :=
match x with
| .ok a => pure a
| .error es => modify (· ++ es) *> pure default
/-- Run the decode action. If it fails, add the errors to the state and return `Inhabited.default`. -/
@[inline] def tryDecode [Inhabited α] (x : Except (Array ε) α) : StateM (Array ε) α :=
tryDecodeD default x
/--
If the value is not `none`, run the decode action.
If it fails, add the errors to the state and return `default`.
-/
@[inline] def optDecodeD (default : β) (a? : Option α) (f : α → Except (Array ε) β) : StateM (Array ε) β :=
match a? with
| some a => tryDecodeD default (f a)
| none => pure default
/--
If the value is not `none`, run the decode action.
If it fails, add the errors to the state and return `Inhabited.default`.
-/
@[inline] def optDecode [Inhabited β] (a? : Option α) (f : α → Except (Array ε) β) : StateM (Array ε) β :=
optDecodeD default a? f
/--
If the value is not `none`, run the decode action.
If it fails, add the errors to the state and return `none`.
Otherwise, return the the result in `some`.
-/
@[inline] def optDecode? (a? : Option α) (f : α → Except (Array ε) β) : StateM (Array ε) (Option β) :=
optDecodeD none a? fun a => some <$> f a
/--
If either action errors, throw the concatenated errors.
Otherwise, if no errors, combine the results with `f`.
-/
def mergeErrors (x₁ : Except (Array ε) α) (x₂ : Except (Array ε) β) (f : α → β → γ) : Except (Array ε) γ :=
match x₁, x₂ with
| .ok a, .ok b => .ok (f a b)
| .ok _, .error es => .error es
| .error es, .ok _ => .error es
| .error es', .error es => .error (es ++ es')
structure Toml.DecodeError where
ref : Syntax
msg : String
class DecodeToml (α : Type u) where
decode (v : Value) : Except (Array DecodeError) α
abbrev decodeToml [DecodeToml α] (v : Value) : Except (Array DecodeError) α :=
DecodeToml.decode v
namespace Toml
/-- Decode an array of TOML values, merging any errors from the elements into a single array. -/
def decodeArray [dec : DecodeToml α] (vs : Array Value) : Except (Array DecodeError) (Array α) :=
vs.foldl (init := Except.ok (.mkEmpty vs.size)) fun vs v =>
mergeErrors vs (dec.decode v) Array.push
instance : DecodeToml Value := ⟨pure⟩
namespace Value
@[inline] def decodeString : Value → Except DecodeError String
| .string _ v => .ok v
| x => .error (.mk x.ref "expected string")
instance : DecodeToml String := ⟨(·.decodeString)⟩
instance : DecodeToml System.FilePath := ⟨(.mk <$> decodeToml ·)⟩
@[inline] def decodeName (v : Value) : Except DecodeError Name := do
match (← v.decodeString).toName with
| .anonymous => throw (.mk v.ref "expected name")
| n => pure n
instance : DecodeToml Lean.Name := ⟨(·.decodeName)⟩
@[inline] def decodeInt : Value → Except DecodeError Int
| .integer _ v => .ok v
| x => .error (.mk x.ref "expected integer")
instance : DecodeToml Int := ⟨(·.decodeInt)⟩
@[inline] def decodeNat : Value → Except DecodeError Nat
| .integer _ (.ofNat v) => .ok v
| x => .error (.mk x.ref "expected nonnegative integer")
instance : DecodeToml Nat := ⟨(·.decodeNat)⟩
@[inline] def decodeFloat : Value → Except DecodeError Float
| .float _ v => .ok v
| x => .error (.mk x.ref "expected float")
instance : DecodeToml Float := ⟨(·.decodeFloat)⟩
@[inline] def decodeBool : Value → Except DecodeError Bool
| .boolean _ v => .ok v
| x => .error (.mk x.ref "expected boolean")
instance : DecodeToml Bool := ⟨(·.decodeBool)⟩
@[inline] def decodeDateTime : Value → Except DecodeError DateTime
| .dateTime _ v => .ok v
| x => .error (.mk x.ref "expected date-time")
instance : DecodeToml DateTime := ⟨(·.decodeDateTime)⟩
@[inline] def decodeValueArray : Value → Except DecodeError (Array Value)
| .array _ vs => .ok vs
| x => .error (.mk x.ref "expected array")
@[inline] protected def decodeArray [dec : DecodeToml α] (v : Value) : Except (Array DecodeError) (Array α) := do
decodeArray (dec := dec) (← v.decodeValueArray)
instance [DecodeToml α] : DecodeToml (Array α) := ⟨Value.decodeArray⟩
@[inline] def decodeArrayOrSingleton [dec : DecodeToml α] : Value → Except (Array DecodeError) (Array α)
| .array _ vs => decodeArray (dec := dec) vs
| v => Array.singleton <$> dec.decode v
@[inline] def decodeTable : Value → Except DecodeError Table
| .table _ t => .ok t
| x => .error (.mk x.ref "expected table")
instance : DecodeToml Table := ⟨(·.decodeTable)⟩
end Value
namespace Table
@[inline] def decodeValue (t : Table) (k : Name) (ref := Syntax.missing) : Except DecodeError Value := do
let some a := t.find? k
| throw (.mk ref s!"missing required key: {ppKey k}")
return a
def decode [dec : DecodeToml α] (t : Table) (k : Name) (ref := Syntax.missing) : Except (Array DecodeError) α := do
let a ← t.decodeValue k ref
dec.decode a |>.mapError fun xs => xs.map fun x =>
{x with msg := s!"key {ppKey k}: " ++ x.msg}
def decodeNameMap [dec : DecodeToml α] (t : Toml.Table) : Except (Array DecodeError) (NameMap α) := do
t.items.foldl (init := Except.ok {}) fun m (k,v) =>
mergeErrors m (dec.decode v) fun m v => m.insert k v
instance [DecodeToml α] : DecodeToml (NameMap α) := ⟨(do decodeNameMap <| ← ·.decodeTable)⟩
@[inline] protected def tryDecode [Inhabited α] [dec : DecodeToml α] (t : Table) (k : Name) (ref := Syntax.missing) : StateM (Array DecodeError) α := do
tryDecode <| t.decode (dec := dec) k ref
@[inline] protected def tryDecode? [dec : DecodeToml α] (t : Table) (k : Name) : StateM (Array DecodeError) (Option α) :=
optDecode? (t.find? k) dec.decode
@[inline] protected def tryDecodeD [dec : DecodeToml α] (k : Name) (default : α) (t : Table) : StateM (Array DecodeError) α :=
optDecodeD default (t.find? k) dec.decode
end Table

13
src/lake/Lake/Toml/Elab.lean Normal file
View file

@ -0,0 +1,13 @@
/-
Copyright (c) 2024 Mac Malone. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Mac Malone
-/
import Lake.Toml.Elab.Expression
/-!
# TOML Elaboration
Elaborates TOML syntax into Lean data types.
At top-level, elaborates a whole TOML file into a `Toml.Table`.
-/

241
src/lake/Lake/Toml/Elab/Expression.lean Normal file
View file

@ -0,0 +1,241 @@
/-
Copyright (c) 2024 Mac Malone. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Mac Malone
-/
import Lake.Toml.Elab.Value
/-!
# TOML Expression Elaboration
Elaborates top-level TOML syntax into a Lean `Toml.Table`.
-/
open Lean
namespace Lake.Toml
/-- The manner in which a TOML key was declared. -/
inductive KeyTy
/-- A key declared via `key = v`. -/
| value
/-- A key declared via `[key]`. -/
| stdTable
/-- A key declared via `[[key]]`. -/
| array
/-- A key declared via `key.foo`. -/
| dottedPrefix
/-- A key declared via `[key.foo]` or `[[key.foo]]`. -/
| headerPrefix
deriving Inhabited
protected def KeyTy.toString (ty : KeyTy) :=
match ty with
| .value => "value"
| .stdTable => "table"
| .array => "array"
| .dottedPrefix => "dotted"
| .headerPrefix => "dotted"
instance : ToString KeyTy := ⟨KeyTy.toString⟩
def KeyTy.isValidPrefix (ty : KeyTy) :=
match ty with
| .stdTable | .headerPrefix | .dottedPrefix => true
| _ => false
structure Keyval where
ref : Syntax
key : Name
val : Value
structure ElabState where
keyTys : NameMap KeyTy := {}
arrKeyTys : NameMap (NameMap KeyTy) := {}
arrParents : NameMap Name := {}
currArrKey : Name := .anonymous
currKey : Name := .anonymous
items : Array Keyval := {}
deriving Inhabited
abbrev TomlElabM := StateT ElabState CoreM
def elabSubKeys (ks : Array (TSyntax ``simpleKey)) : TomlElabM Name := do
ks.foldlM (init := (← get).currKey) fun k kStx => do
let k := k.str <| ← elabSimpleKey kStx
if let some ty := (← get).keyTys.find? k then
unless ty matches .dottedPrefix do
throwErrorAt kStx "cannot redefine {ty} key '{k}'"
else
modify fun s => {s with keyTys := s.keyTys.insert k .dottedPrefix}
return k
def elabKeyval (kv : TSyntax ``keyval) : TomlElabM Unit := do
let `(keyval|$kStx = $v) := kv
| throwErrorAt kv "ill-formed key-value pair syntax"
let `(key|$[$ks:simpleKey].*) := kStx
| throwErrorAt kStx "ill-formed key syntax"
let tailKeyStx := ks.back
let k ← elabSubKeys ks.pop
let k := k.str <| ← elabSimpleKey tailKeyStx
if let some ty := (← get).keyTys.find? k then
throwErrorAt tailKeyStx "cannot redefine {ty} key '{k}'"
else
let v ← elabVal v
modify fun s => {
s with
items := s.items.push ⟨kStx, k, v⟩
keyTys := s.keyTys.insert k .value
}
def elabHeaderKeys (ks : Array (TSyntax ``simpleKey)) : TomlElabM Name := do
modify fun s =>
let arrKeyTys := s.arrKeyTys.insert s.currArrKey s.keyTys
{
s with
arrKeyTys
currArrKey := .anonymous
keyTys := arrKeyTys.find? .anonymous |>.getD {}
}
ks.foldlM (init := Name.anonymous) fun k kStx => do
let k ← k.str <$> elabSimpleKey kStx
if let some ty := (← get).keyTys.find? k then
match ty with
| .array =>
let some keyTys := (← get).arrKeyTys.find? k
| throwError "(internal) bad array key '{k}'"
modify fun s => {s with keyTys, currArrKey := k}
| .stdTable | .headerPrefix | .dottedPrefix => pure ()
| _ => throwErrorAt kStx m!"cannot redefine {ty} key '{k}'"
else
modify fun s => {s with keyTys := s.keyTys.insert k .headerPrefix}
return k
def elabStdTable (x : TSyntax ``stdTable) : TomlElabM Unit := withRef x do
let `(stdTable|[$kStx]) := x
| throwErrorAt x "ill-formed table syntax"
let `(key|$[$ks:simpleKey].*) := kStx
| throwErrorAt kStx "ill-formed key syntax"
let tailKey := ks.back
let k ← elabHeaderKeys ks.pop
let k ← k.str <$> elabSimpleKey tailKey
if let some ty := (← get).keyTys.find? k then
unless ty matches .headerPrefix do
throwErrorAt tailKey m!"cannot redefine {ty} key '{k}'"
modify fun s => {
s with
currKey := k
keyTys := s.keyTys.insert k .stdTable
items := s.items.push ⟨x, k, .table x {}⟩
}
def elabArrayTable (x : TSyntax ``arrayTable) : TomlElabM Unit := withRef x do
let `(arrayTable|[[$k]]) := x
| throwErrorAt x "ill-formed array table syntax"
let `(key|$[$ks:simpleKey].*) := k
| throwErrorAt x "ill-formed key syntax"
let tailKey := ks.back
let k ← elabHeaderKeys ks.pop
let k := k.str (← elabSimpleKey tailKey)
if let some ty := (← get).keyTys.find? k then
if ty matches .array then
let s ← get
let some keyTys := s.arrParents.find? k >>= s.arrKeyTys.find?
| throwError "(internal) bad array key '{k}'"
modify fun s => {
s with
keyTys, currKey := k, currArrKey := k
items := s.items.push ⟨x, k, .array x #[.table x {}]⟩
}
else
throwErrorAt tailKey s!"cannot redefine {ty} key '{k}'"
else
modify fun s =>
let keyTys := s.keyTys.insert k .array
{
s with
keyTys
currKey := k
currArrKey := k
arrKeyTys := s.arrKeyTys.insert s.currArrKey keyTys
arrParents := s.arrParents.insert k s.currArrKey
items := s.items.push ⟨x, k, .array x #[.table x {}]⟩
}
def elabExpression (x : TSyntax ``expression) : TomlElabM Unit := do
match x with
| `(expression|$x:keyval) => elabKeyval x
| `(expression|$x:stdTable) => elabStdTable x
| `(expression|$x:arrayTable) => elabArrayTable x
| _ => throwErrorAt x "ill-formed expression syntax"
/--
Construct a table of simple key-value pairs from arbitrary key-value pairs.
For example:
`{a.b := [c.d := 0]}, {a.b := [c.e := 1]}`
becomes
`{a := {b := [{c := {d := 0, e := 1}}]}}`
-/
partial def mkSimpleTable (items : Array Keyval) : Table :=
items.foldl (init := {}) fun t ⟨kRef,k,v⟩ =>
match k.components with
| .nil => t
| .cons k ks => insert t kRef k ks v
where
simpVal : Value → Value
| .table ref t => .table ref <| t.items.foldl (init := {}) fun t ⟨k,v⟩ =>
match k.components with
| .nil => t
| .cons k ks => insert t ref k ks v
| .array ref vs => .array ref <| vs.map simpVal
| v => v
insert t kRef k ks newV :=
match ks with
| .nil => t.alter k fun v? =>
match v?, simpVal newV with
| some (.table ref vt), .table _ newT => .table ref (vt ++ newT)
| some (.array ref vs), .array _ newVs => .array ref (vs ++ newVs)
| some (.array ref vs), newV => .array ref (vs.push newV)
| _, newV => newV
| k' :: ks => t.alter k fun v? =>
if let some v := v? then
match v with
| .array ref vs =>
.array ref <| vs.modify (vs.size-1) fun
| .table ref t' => .table ref <| insert t' kRef k' ks newV
| _ => .table kRef {}
| .table ref t' => .table ref <| insert t' kRef k' ks newV
| _ => .table kRef <| insert {} kRef k' ks newV
else
.table kRef <| insert {} kRef k' ks newV
nonrec def TomlElabM.run (x : TomlElabM Unit) : CoreM Table := do
let (_,s) ← x.run {}
return mkSimpleTable s.items
def elabToml (x : TSyntax ``toml) : CoreM Table := do
let `(toml|$xs*) := x
| throwErrorAt x "ill-formed TOML syntax"
TomlElabM.run do
let mut recovering := false
for x in xs.getElems do
try
match x with
| `(expression|$x:keyval) =>
unless recovering do
elabKeyval x
| `(expression|$x:stdTable) =>
elabStdTable x
recovering := false
| `(expression|$x:arrayTable) =>
elabArrayTable x
recovering := false
| _ =>
logErrorAt x "ill-formed expression syntax"
catch e : Exception =>
recovering := true
logErrorAt e.getRef e.toMessageData

243
src/lake/Lake/Toml/Elab/Value.lean Normal file
View file

@ -0,0 +1,243 @@
/-
Copyright (c) 2024 Mac Malone. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Mac Malone
-/
import Lean.CoreM
import Lake.Toml.Data.Value
import Lake.Toml.Grammar
/-!
# TOML Value Elaboration
Elaborates TOML values into Lean data types.
-/
open Lean
namespace Lake.Toml
@[inline] def elabLit {k : SyntaxNodeKind} (x : TSyntax k) (name : String) : CoreM String := do
let some spelling := x.raw.isLit? k
| throwErrorAt x s!"ill-formed {name} syntax"
return spelling
def elabBoolean (x : TSyntax ``boolean) : CoreM Bool := do
match x with
| `(boolean|true)=> return true
| `(boolean|false) => return false
| _ => throwErrorAt x "invalid boolean"
--------------------------------------------------------------------------------
/-! ## Numerals -/
--------------------------------------------------------------------------------
def decodeDecNum (s : String) : Nat :=
s.foldl (init := 0) fun n c =>
if c == '_' then n else n*10 + (c.val - '0'.val).toNat
def decodeSign (s : String) : Bool × String :=
if s.front == '-' then
(true, s.drop 1)
else if s.front == '+' then
(false, s.drop 1)
else
(false, s)
def decodeDecInt (s : String) : Int :=
let (sign, s) := decodeSign s
if sign then
.negOfNat <| decodeDecNum s
else
.ofNat <| decodeDecNum s
def elabDecInt (x : TSyntax ``decInt) : CoreM Int := do
return decodeDecInt <| ← elabLit x "decimal integer"
def decodeMantissa (s : String) : Nat × Nat :=
let (m,e) := s.foldl (init := (0,s.length)) fun (m,e) c =>
match c with
| '_' => (m,e)
| '.' => (m,0)
| c => (m*10 + (c.val - '0'.val).toNat, e+1)
(m, if e ≥ s.length then 0 else e)
def decodeFrExp (s : String) : Nat × Int :=
match s.split (fun c => c == 'E' || c == 'e') with
| [m,exp] =>
let exp := decodeDecInt exp
let (m,dotExp) := decodeMantissa m
(m, Int.negOfNat dotExp + exp)
| [m] =>
let (m, e) := decodeMantissa m
(m, Int.negOfNat e)
| _ => (0,0)
def decodeFloat (s : String) : Float :=
let (sign, s) := decodeSign s
if s = "inf" then
if sign then -1.0/0 else 1.0/0
else if s = "nan" then
if sign then -(0.0/0) else 0.0/0
else
let (m,e) := decodeFrExp s
let flt := Float.ofScientific m (e < 0) e.natAbs
if sign then -flt else flt
def elabFloat (x : TSyntax ``float) : CoreM Float := do
return decodeFloat <| ← elabLit x "float"
def elabBinNum (x : TSyntax ``binNum) : CoreM Nat := do
let spelling ← elabLit x "binary number"
return spelling.drop 2 |>.foldl (init := 0) fun n c =>
if c == '_' then n else n*2 + (c.val - '0'.val).toNat
def elabOctNum (x : TSyntax ``octNum) : CoreM Nat := do
let spelling ← elabLit x "octal number"
return spelling.drop 2 |>.foldl (init := 0) fun n c =>
if c == '_' then n else n*8 + (c.val - '0'.val).toNat
def decodeHexDigit (c : Char) : Nat :=
if c ≤ '9' then (c.val - '0'.val).toNat
else if c ≤ 'F' then 10 + (c.val - 'A'.val).toNat
else 10 + (c.val - 'a'.val).toNat
def elabHexNum (x : TSyntax ``hexNum) : CoreM Nat := do
let spelling ← elabLit x "hexadecimal number"
return spelling.drop 2 |>.foldl (init := 0) fun n c =>
if c == '_' then n else n*16 + decodeHexDigit c
def elabDateTime (x : TSyntax ``dateTime) : CoreM DateTime := do
let spelling ← elabLit x "date-time"
let some dt := DateTime.ofString? spelling
| throwErrorAt x "invalid date-time"
return dt
--------------------------------------------------------------------------------
/-! ## Strings & Simple Keys -/
--------------------------------------------------------------------------------
def elabLiteralString (x : TSyntax ``literalString) : CoreM String := do
return (← elabLit x "literalString").drop 1 |>.dropRight 1
def decodeHexDigits (s : Substring) : Nat :=
s.foldl (init := 0) fun n c => n*16 + decodeHexDigit c
partial def elabBasicStringCore (lit : String) (i : String.Pos := 0) (out := "") : CoreM String := do
if h : lit.atEnd i then
return out
else
let curr := lit.get' i h
let i := lit.next' i h
if curr == '\\' then
if h : lit.atEnd i then
return out
else
let curr := lit.get' i h
let elabUnicodeEscape escape :=
let val := decodeHexDigits escape
if h : val.isValidChar then
let ch := Char.ofNatAux val h
elabBasicStringCore lit escape.stopPos (out.push ch)
else
throwError "invalid unicode escape '{escape}'"
match curr with
| 'b' => elabBasicStringCore lit (lit.next' i h) (out.push '\x08')
| 't' => elabBasicStringCore lit (lit.next' i h) (out.push '\t')
| 'n' => elabBasicStringCore lit (lit.next' i h) (out.push '\n')
| 'f' => elabBasicStringCore lit (lit.next' i h) (out.push '\x0C')
| 'r' => elabBasicStringCore lit (lit.next' i h) (out.push '\r')
| '\"' => elabBasicStringCore lit (lit.next' i h) (out.push '"')
| '\\' => elabBasicStringCore lit (lit.next' i h) (out.push '\\')
| 'u' => elabUnicodeEscape (Substring.mk lit (lit.next' i h) lit.endPos |>.take 4)
| 'U' => elabUnicodeEscape (Substring.mk lit (lit.next' i h) lit.endPos |>.take 8)
| _ =>
let i := Substring.mk lit i lit.endPos |>.trimLeft |>.startPos
elabBasicStringCore lit i out
else
elabBasicStringCore lit i (out.push curr)
def elabBasicString (x : TSyntax ``basicString) : CoreM String := do
let spelling ← elabLit x "basic string"
withRef x <| elabBasicStringCore (spelling.drop 1 |>.dropRight 1)
def dropInitialNewline (s : String) : String :=
if s.front == '\r' then
s.drop 2
else if s.front == '\n' then
s.drop 1
else
s
def elabMlLiteralString (x : TSyntax ``mlLiteralString) : CoreM String := do
let spelling ← elabLit x "multi-line literal string"
return dropInitialNewline (spelling.drop 3 |>.dropRight 3)
def elabMlBasicString (x : TSyntax ``mlBasicString) : CoreM String := do
let spelling ← elabLit x "multi-line basic string"
withRef x <| elabBasicStringCore (dropInitialNewline (spelling.drop 3 |>.dropRight 3))
def elabString (x : TSyntax ``string) : CoreM String := do
match x with
| `(val|$x:literalString) => elabLiteralString x
| `(val|$x:basicString) => elabBasicString x
| `(val|$x:mlLiteralString) => elabMlLiteralString x
| `(val|$x:mlBasicString) => elabMlBasicString x
| _ => throwErrorAt x "ill-formed string syntax"
@[inline] def elabUnquotedKey (x : TSyntax ``unquotedKey) : CoreM String := do
elabLit x "unquoted key"
def elabSimpleKey (x : TSyntax ``simpleKey) : CoreM String := do
match x with
| `(simpleKey|$x:unquotedKey) => elabUnquotedKey x
| `(simpleKey|$x:literalString) => elabLiteralString x
| `(simpleKey|$x:basicString) => elabBasicString x
| _ => throwErrorAt x "ill-formed simple key syntax"
--------------------------------------------------------------------------------
/-! ## Complex Values -/
--------------------------------------------------------------------------------
def elabArray (x : TSyntax ``array) (elabVal : TSyntax ``val → CoreM α) : CoreM (Array α) := do
let `(val|[$xs,*]) := x
| throwErrorAt x "ill-formed array syntax"
xs.getElems.mapM elabVal
def elabInlineTable (x : TSyntax ``inlineTable) (elabVal : TSyntax ``val → CoreM Value) : CoreM Table := do
let `(val|{$kvs,*}) := x
| throwErrorAt x "ill-formed inline table syntax"
let t : NameDict (Option Value) := {} -- some: static value, none: partial table
let t ← kvs.getElems.foldlM (init := t) fun t kv => do
let `(keyval|$k = $v) := kv
| throwErrorAt kv "ill-formed key-value pair syntax"
let `(key|$[$ks].*) := k
| throwErrorAt k "ill-formed key syntax"
let tailKey := ks.back
let (k, t) ← StateT.run (s := t) <| ks.pop.foldlM (init := Name.anonymous) fun k p => do
let k ← k.str <$> elabSimpleKey p
if let some v := t.find? k then
unless v.isNone do throwErrorAt p m!"cannot redefine key '{k}'"
else
modify fun t => t.push k none
return k
let k ← k.str <$> elabSimpleKey tailKey
if t.contains k then
throwErrorAt tailKey m!"cannot redefine key '{k}'"
else
return t.push k (← elabVal v)
return t.filterMap fun _ v => v
partial def elabVal (x : TSyntax ``val) : CoreM Value := do
match x with
| `(val|$x:float) => .float x <$> elabFloat x
| `(val|$x:decInt) => .integer x <$> elabDecInt x
| `(val|$x:binNum) => .integer x <$> .ofNat <$> elabBinNum x
| `(val|$x:octNum) => .integer x <$> .ofNat <$> elabOctNum x
| `(val|$x:hexNum) => .integer x <$> .ofNat <$> elabHexNum x
| `(val|$x:dateTime) => .dateTime x <$> elabDateTime x
| `(val|$x:string) => .string x <$> elabString x
| `(val|$x:boolean) => .boolean x <$> elabBoolean x
| `(val|$x:array) => .array x <$> elabArray x elabVal
| `(val|$x:inlineTable) => .table x <$> elabInlineTable x elabVal
| _ => throwErrorAt x "ill-formed value syntax"

74
src/lake/Lake/Toml/Encode.lean Normal file
View file

@ -0,0 +1,74 @@
/-
Copyright (c) 2024 Mac Malone. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Mac Malone
-/
import Lake.Toml.Data
import Lake.Util.FilePath
/-!
# TOML Encoders
This module contains definitions to assist in encoding Lean types
into TOML data values.
-/
namespace Lake
open System Lean Toml
class ToToml (α : Type u) where
toToml : α → Value
export ToToml (toToml)
instance : ToToml Value := ⟨id⟩
instance : ToToml String := ⟨.string .missing⟩
instance : ToToml FilePath := ⟨(toToml <| mkRelPathString ·)⟩
instance : ToToml Name := ⟨(toToml ·.toString)⟩
instance : ToToml Int := ⟨.integer .missing⟩
instance : ToToml Nat := ⟨fun n => .integer .missing (.ofNat n)⟩
instance : ToToml Float := ⟨.float .missing⟩
instance : ToToml Bool := ⟨.boolean .missing⟩
instance [ToToml α] : ToToml (Array α) := ⟨(.array .missing <| ·.map toToml)⟩
instance : ToToml Table := ⟨.table .missing⟩
/-- Insert a value into a table unless it represents a nullish value. -/
class SmartInsert (α : Type u) where
smartInsert (k : Name) : α → Table → Table
namespace Toml.Table
/-- Inserts the encoded value into the table. -/
@[inline] nonrec def insert [enc : ToToml α] (k : Name) (v : α) (t : Table) : Table :=
t.insert k (enc.toToml v)
instance (priority := low) [ToToml α] : SmartInsert α := ⟨Table.insert⟩
/-- If the value is not `none`, inserts the encoded value into the table. -/
@[inline] nonrec def insertSome [enc : ToToml α] (k : Name) (v? : Option α) (t : Table) : Table :=
t.insertSome k (v?.map enc.toToml)
instance [ToToml α] : SmartInsert (Option α) := ⟨Table.insertSome⟩
/-- Insert a value into the table unless it represents a nullish value. -/
@[inline] nonrec def smartInsert [SmartInsert α] (k : Name) (v : α) (t : Table) : Table :=
SmartInsert.smartInsert k v t
instance : SmartInsert Table where
smartInsert k v t := t.insertUnless v.isEmpty k (toToml v)
instance [ToToml (Array α)] : SmartInsert (Array α) where
smartInsert k v t := t.insertUnless v.isEmpty k (toToml v)
/-- Insert a value into the table if `p` is `true`. -/
@[inline] nonrec def insertIf [enc : ToToml α] (p : Bool) (k : Name) (v : α) (t : Table) : Table :=
t.insertIf p k (enc.toToml v)
/-- Insert a value into the table if `p` is `false`. -/
@[inline] nonrec def insertUnless [enc : ToToml α] (p : Bool) (k : Name) (v : α) (t : Table) : Table :=
t.insertUnless p k (enc.toToml v)
/-- Inserts the value into the table if it is not equal to `default`. -/
@[inline] def insertD [enc : ToToml α] [BEq α] (k : Name) (v : α) (default : α) (t : Table) : Table :=
t.insertUnless (v == default) k (enc.toToml v)

647
src/lake/Lake/Toml/Grammar.lean Normal file
View file

@ -0,0 +1,647 @@
/-
Copyright (c) 2024 Mac Malone. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Mac Malone
-/
import Lake.Toml.ParserUtil
/-!
# TOML Grammar
A Lean encoding of the v1.0.0 TOML grammar ([en][1], [abnf]][2])
using `Lean.Parser` objects. The current encoding elides the use of
tokens entirely, relying purely on custom parser functions.
[1]: https://toml.io/en/v1.0.0
[2]: https://github.com/toml-lang/toml/blob/1.0.0/toml.abnf
-/
namespace Lake.Toml
open Lean Parser
/-- Is it a TOML control character? (excludes tabs and spaces) -/
def isControlChar (c : Char) :=
c = '\x7F' || (c < '\x20' && c != '\t')
--------------------------------------------------------------------------------
/-! ## Trailing Functions -/
--------------------------------------------------------------------------------
/-- Consume optional horizontal whitespace (i.e., tab or space). -/
def wsFn : ParserFn :=
takeWhileFn fun c => c = ' ' || c = '\t'
/-- Consumes the LF following a CR in a CRLF newline. -/
def crlfAuxFn : ParserFn := fun c s =>
let input := c.input
let errMsg := "invalid newline; no LF after CR"
if h : input.atEnd s.pos then
s.mkUnexpectedError errMsg
else
let curr := input.get' s.pos h
if curr == '\n' then
s.next' input s.pos h
else
s.mkUnexpectedError errMsg
/-- Consume a newline. -/
def newlineFn : ParserFn := fun c s =>
let input := c.input
if h : input.atEnd s.pos then
s.mkEOIError ["newline"]
else
let curr := input.get' s.pos h
if curr == '\n' then
s.next' input s.pos h
else if curr == '\r' then
crlfAuxFn c (s.next' input s.pos h)
else
mkUnexpectedCharError s curr ["newline"]
/-- Consumes the body of a comment. -/
def commentBodyFn : ParserFn :=
-- While the v1.0.0 TOML ABNF grammar permits a `DEL`, the test suite does not.
-- We forbid it because it the omission seems likely to be an error
takeUntilFn isControlChar
/-- Consumes a line comment. -/
def commentFn : ParserFn :=
chFn '#' ["comment"] >> commentBodyFn
/-- Consume optional whitespace (space, tab, or newline). -/
partial def wsNewlineFn : ParserFn := fun c s =>
let input := c.input
if h : input.atEnd s.pos then
s
else
let curr := input.get' s.pos h
if curr = ' ' || curr = '\t' || curr == '\n' then
wsNewlineFn c (s.next' input s.pos h)
else if curr == '\r' then
(crlfAuxFn >> wsNewlineFn) c (s.next' input s.pos h)
else
s
/-- Consume optional sequence of whitespace / newline(s) / comment (s). -/
partial def trailingFn : ParserFn := fun c s =>
let input := c.input
if h : input.atEnd s.pos then
s
else
let curr := input.get' s.pos h
if curr = ' ' || curr = '\t' || curr == '\n' then
trailingFn c (s.next' input s.pos h)
else if curr == '\r' then
(crlfAuxFn >> trailingFn) c (s.next' input s.pos h)
else if curr == '#' then
(commentBodyFn >> trailingFn) c (s.next' input s.pos h)
else
s
--------------------------------------------------------------------------------
/-! ## Strings -/
--------------------------------------------------------------------------------
/-- A TOML character escape. -/
def isEscapeChar (c : Char) : Bool :=
c == 'b' || c == 't' || c == 'n' || c == 'f' || c == 'r' || c == '\"' || c == '\\'
/-- Consumes a TOML string escape sequence after a `\`. -/
def escapeSeqFn (stringGap : Bool) : ParserFn := fun c s =>
let input := c.input
let expected := ["escape sequence"]
if h : input.atEnd s.pos then
s.mkEOIError expected
else
let curr := input.get' s.pos h
let ifStringGap (p : ParserFn) :=
if stringGap then
p c (s.next' input s.pos h)
else
s.mkUnexpectedError "string gap is forbidden here" expected
if isEscapeChar curr then
s.next' input s.pos h
else if curr == 'u' then
repeatFn 4 hexDigitFn c (s.next' input s.pos h)
else if curr == 'U' then
repeatFn 8 hexDigitFn c (s.next' input s.pos h)
else if curr == ' ' || curr == '\t' then
ifStringGap (wsFn >> newlineFn >> wsNewlineFn)
else if curr == '\n' then
ifStringGap wsNewlineFn
else if curr == '\r' then
ifStringGap (crlfAuxFn >> wsNewlineFn)
else
s.mkUnexpectedError "invalid escape sequence"
partial def basicStringAuxFn (startPos : String.Pos) : ParserFn := fun c s =>
let input := c.input
if h : input.atEnd s.pos then
s.mkUnexpectedErrorAt "unterminated basic string" startPos
else
let curr := input.get' s.pos h
if curr == '\"' then
s.next' input s.pos h
else if curr == '\\' then
(escapeSeqFn false >> basicStringAuxFn startPos) c (s.next' input s.pos h)
else if isControlChar curr then
mkUnexpectedCharError s curr
else
basicStringAuxFn startPos c (s.next' input s.pos h)
def basicStringFn : ParserFn := usePosFn fun startPos =>
chFn '\"' ["basic string"] >> basicStringAuxFn startPos
partial def literalStringAuxFn (startPos : String.Pos) : ParserFn := fun c s =>
let input := c.input
if h : input.atEnd s.pos then
s.mkUnexpectedErrorAt "unterminated literal string" startPos
else
let curr := input.get' s.pos h
if curr == '\'' then
s.next' input s.pos h
else if isControlChar curr then
mkUnexpectedCharError s curr
else
literalStringAuxFn startPos c (s.next' input s.pos h)
def literalStringFn : ParserFn := usePosFn fun startPos =>
chFn '\'' ["literal string"] >> literalStringAuxFn startPos
partial def mlLiteralStringAuxFn (startPos : String.Pos) (quoteDepth : Nat) : ParserFn := fun c s =>
let input := c.input
if h : input.atEnd s.pos then
if quoteDepth ≥ 3 then
s
else
s.mkUnexpectedErrorAt "unterminated multi-line literal string" startPos
else
let curr := input.get' s.pos h
if curr == '\'' then
let s := s.next' input s.pos h
if quoteDepth ≥ 5 then
s.mkUnexpectedError "too many quotes"
else
mlLiteralStringAuxFn startPos (quoteDepth+1) c s
else if quoteDepth ≥ 3 then
s
else if curr == '\n' then
mlLiteralStringAuxFn startPos 0 c (s.next' input s.pos h)
else if curr == '\r' then
(crlfAuxFn >> mlLiteralStringAuxFn startPos 0) c (s.next' input s.pos h)
else if isControlChar curr then
mkUnexpectedCharError s curr
else
mlLiteralStringAuxFn startPos 0 c (s.next' input s.pos h)
def mlLiteralStringFn : ParserFn := usePosFn fun startPos =>
atomicFn (repeatFn 3 (chFn '\'' ["multi-line literal string"])) >>
mlLiteralStringAuxFn startPos 0
partial def mlBasicStringAuxFn (startPos : String.Pos) (quoteDepth : Nat) : ParserFn := fun c s =>
let input := c.input
if h : input.atEnd s.pos then
if quoteDepth ≥ 3 then
s
else
s.mkUnexpectedErrorAt "unterminated multi-line basic string" startPos
else
let curr := input.get' s.pos h
if curr == '\"' then
let s := s.next' input s.pos h
if quoteDepth ≥ 5 then
s.mkUnexpectedError "too many quotes"
else
mlBasicStringAuxFn startPos (quoteDepth+1) c s
else if quoteDepth ≥ 3 then
s
else if curr == '\n' then
mlBasicStringAuxFn startPos 0 c (s.next' input s.pos h)
else if curr == '\r' then
(crlfAuxFn >> mlBasicStringAuxFn startPos 0) c (s.next' input s.pos h)
else if curr == '\\' then
(escapeSeqFn true >> mlBasicStringAuxFn startPos 0) c (s.next' input s.pos h)
else if isControlChar curr then
mkUnexpectedCharError s curr
else
mlBasicStringAuxFn startPos 0 c (s.next' input s.pos h)
def mlBasicStringFn : ParserFn := usePosFn fun startPos =>
atomicFn (repeatFn 3 (chFn '\"' ["multi-line basic string"])) >>
mlBasicStringAuxFn startPos 0
--------------------------------------------------------------------------------
/-! ## Numerals (Date-Times, Floats, and Integers) -/
--------------------------------------------------------------------------------
def hourMinFn : ParserFn :=
digitPairFn ["hour digit"] >> chFn ':' >> digitPairFn ["minute digit"]
def timeTailFn (allowOffset : Bool) : ParserFn := fun c s =>
let input := c.input
if h : input.atEnd s.pos then
s
else
let curr := input.get' s.pos h
if curr = '.' then
let s := s.next' input s.pos h
let s := takeWhile1Fn (·.isDigit) ["millisecond"] c s
if s.hasError then s else
if h : input.atEnd s.pos then s else
timeOffsetFn (input.get' s.pos h) (input.next' s.pos h) c s
else
timeOffsetFn curr (input.next' s.pos h) c s
where
@[inline] timeOffsetFn curr nextPos c s :=
if curr == 'Z' || curr == 'z' then
if allowOffset then s.setPos nextPos else
s.mkUnexpectedError "time offset is forbidden here"
else if curr = '+' || curr = '-' then
if allowOffset then hourMinFn c (s.setPos nextPos) else
s.mkUnexpectedError "time offset is forbidden here"
else
s
def timeAuxFn (allowOffset : Bool) : ParserFn :=
digitPairFn ["minute digit"] >> chFn ':' >>
digitPairFn ["second digit"] >> timeTailFn allowOffset
def timeFn (allowOffset := false) : ParserFn :=
digitPairFn ["hour"] >> chFn ':' >> timeAuxFn allowOffset
def optTimeFn : ParserFn := fun c s =>
let i := s.pos
let input := c.input
if h : input.atEnd i then
s
else
let curr := input.get' i h
if curr = 'T' || curr = 't' then
timeFn true c (s.next' input i h)
else if curr = ' ' then
let tPos := input.next' i h
let s := timeFn true c (s.setPos tPos)
if s.hasError && s.pos == tPos then s.restore (s.stackSize-1) i else s
else
s
def dateTimeAuxFn : ParserFn :=
digitPairFn ["month digit"] >> chFn '-' >>
digitPairFn ["day digit"] >> optTimeFn
def dateTimeFn : ParserFn :=
repeatFn 4 (digitFn ["year digit"]) >> chFn '-' >> dateTimeAuxFn
def dateTimeLitFn : ParserFn :=
litFn `Lake.Toml.dateTime dateTimeFn
def decExpFn : ParserFn := fun c s =>
let input := c.input
let expected := ["decimal exponent"]
if h : input.atEnd s.pos then
s.mkEOIError expected
else
let curr := input.get' s.pos h
if curr = '-' || curr == '+' then
let s := s.next' input s.pos h
sepByChar1Fn (·.isDigit) '_' expected c s
else if curr.isDigit then
let s := s.next' input s.pos h
sepByChar1AuxFn (·.isDigit) '_' expected c s
else
mkUnexpectedCharError s curr expected
def optDecExpFn : ParserFn := fun c s =>
let input := c.input
if h : input.atEnd s.pos then
s
else
let curr := input.get' s.pos h
if curr == 'e' || curr == 'E' then
decExpFn c (s.next' input s.pos h)
else
s
def decNumberTailAuxFn (startPos : String.Pos) (curr : Char) (nextPos : String.Pos) : ParserFn := fun c s =>
if curr == '.' then
let s := s.setPos nextPos
let s := sepByChar1Fn (·.isDigit) '_' ["decimal fraction"] c s
if s.hasError then s else
let s := optDecExpFn c s
if s.hasError then s else
pushLit `Lake.Toml.float startPos skipFn c s
else if curr == 'e' || curr == 'E' then
let s := s.setPos nextPos
let s := decExpFn c s
if s.hasError then s else
pushLit `Lake.Toml.float startPos skipFn c s
else
pushLit `Lake.Toml.decInt startPos skipFn c s
def decNumberTailFn (startPos : String.Pos) : ParserFn := fun c s =>
let input := c.input
if h : input.atEnd s.pos then
pushLit `Lake.Toml.decInt startPos skipFn c s
else
decNumberTailAuxFn startPos (input.get' s.pos h) (input.next' s.pos h) c s
mutual
partial def decNumberSepFn (startPos : String.Pos) (curr : Char) (nextPos : String.Pos) : ParserFn := fun c s =>
if curr == '_' then
let s := s.setPos nextPos
decNumberFn startPos c s
else
decNumberTailAuxFn startPos curr nextPos c s
partial def decNumberAuxFn (startPos : String.Pos) : ParserFn := fun c s =>
let input := c.input
if h : input.atEnd s.pos then
pushLit `Lake.Toml.decInt startPos skipFn c s
else
let curr := input.get' s.pos h
if curr.isDigit then
let s := s.next' input s.pos h
decNumberAuxFn startPos c s
else
decNumberSepFn startPos curr (input.next' s.pos h) c s
partial def decNumberFn (startPos : String.Pos) : ParserFn := fun c s =>
let i := s.pos
let input := c.input
let expected := ["decimal integer", "float"]
if h : input.atEnd i then
s.mkEOIError expected
else
let curr := input.get' i h
if curr.isDigit then
let s := s.next' input i h
decNumberAuxFn startPos c s
else
mkUnexpectedCharError s curr expected
end
def infAuxFn (startPos : String.Pos) : ParserFn :=
strFn "nf" ["'inf'"] >> pushLit `Lake.Toml.float startPos
def nanAuxFn (startPos : String.Pos) : ParserFn :=
strFn "an" ["'nan'"] >> pushLit `Lake.Toml.float startPos
def decimalFn (startPos : String.Pos) : ParserFn := fun c s =>
let input := c.input
let expected := ["decimal integer", "float"]
if h : input.atEnd s.pos then
s.mkEOIError expected
else
let curr := input.get' s.pos h
if curr == '0' then
decNumberTailFn startPos c (s.next' input s.pos h)
else if curr.isDigit then
decNumberAuxFn startPos c (s.next' input s.pos h)
else if curr == 'i' then
infAuxFn startPos c (s.next' input s.pos h)
else if curr == 'n' then
nanAuxFn startPos c (s.next' input s.pos h)
else
mkUnexpectedCharError s curr expected
def decNumeralAuxFn (startPos : String.Pos) : ParserFn := fun c s =>
let input := c.input
if h : input.atEnd s.pos then
s.mkEOIError ["decimal integer", "float", "date-time"]
else -- `NN`
let curr := input.get' s.pos h
let nextPos := input.next' s.pos h
if curr.isDigit then
let s := s.setPos nextPos
if h : input.atEnd s.pos then
pushLit `Lake.Toml.decInt startPos skipFn c s
else
let curr := input.get' s.pos h
let nextPos := input.next' s.pos h
if curr == ':' then -- `HH:`
let s := s.setPos nextPos
let s := timeAuxFn false c s
if s.hasError then s else
pushLit `Lake.Toml.dateTime startPos skipFn c s
else if curr.isDigit then -- `NNN`
let s := s.setPos nextPos
if h : input.atEnd s.pos then
pushLit `Lake.Toml.decInt startPos skipFn c s
else
let curr := input.get' s.pos h
let nextPos := input.next' s.pos h
if curr.isDigit then -- `NNNN`
let s := s.setPos nextPos
if h : input.atEnd nextPos then
pushLit `Lake.Toml.decInt startPos skipFn c s
else
let curr := input.get' s.pos h
let nextPos := input.next' s.pos h
if curr == '-' then -- `YYYY-`
let s := s.setPos nextPos
let s := dateTimeAuxFn c s
if s.hasError then s else
pushLit `Lake.Toml.dateTime startPos skipFn c s
else if curr.isDigit then
let s := s.setPos nextPos
decNumberAuxFn startPos c s
else
decNumberSepFn startPos curr nextPos c s
else
decNumberSepFn startPos curr nextPos c s
else
decNumberSepFn startPos curr nextPos c s
else
decNumberSepFn startPos curr nextPos c s
def numeralFn : ParserFn := atomicFn fun c s =>
let input := c.input
let startPos := s.pos
let expected := ["integer", "float", "date-time"]
if h : input.atEnd s.pos then
s.mkEOIError expected
else
let curr := input.get' s.pos h
if curr == '0' then
let s := s.next' input startPos h
if h : input.atEnd s.pos then
pushLit `Lake.Toml.decInt startPos skipFn c s
else
let curr := input.get' s.pos h
if curr == 'b' then
let s := s.next' input s.pos h
let s := sepByChar1Fn isBinDigit '_' ["binary integer"] c s
if s.hasError then s else
pushLit `Lake.Toml.binNum startPos skipFn c s
else if curr == 'o' then
let s := s.next' input s.pos h
let s := sepByChar1Fn isOctDigit '_' ["octal integer"] c s
if s.hasError then s else
pushLit `Lake.Toml.octNum startPos skipFn c s
else if curr == 'x' then
let s := s.next' input s.pos h
let s := sepByChar1Fn isHexDigit '_' ["hexadecimal integer"] c s
if s.hasError then s else
pushLit `Lake.Toml.hexNum startPos skipFn c s
else if curr.isDigit then
let s := s.next' input s.pos h
let s := (chFn ':' >> timeAuxFn false) c s
if s.hasError then s else
pushLit `Lake.Toml.dateTime startPos skipFn c s
else
decNumberTailAuxFn startPos curr (input.next' s.pos h) c s
else if curr.isDigit then
decNumeralAuxFn startPos c (s.next' input s.pos h)
else if curr == '+' || curr == '-' then
decimalFn startPos c (s.next' input s.pos h)
else if curr == 'i' then
infAuxFn startPos c (s.next' input s.pos h)
else if curr == 'n' then
nanAuxFn startPos c (s.next' input s.pos h)
else
s.mkUnexpectedError s!"unexpected '{curr}'" expected
--------------------------------------------------------------------------------
/-! ## Parsers -/
--------------------------------------------------------------------------------
def trailingWs : Parser :=
trailing wsFn
def trailingSep : Parser :=
trailing trailingFn
def unquotedKeyFn : ParserFn :=
takeWhile1Fn (fun c => c.isAlphanum || c == '_' || c == '-') ["unquoted key"]
def unquotedKey : Parser :=
litWithAntiquot "unquotedKey" `Lake.Toml.unquotedKey unquotedKeyFn
def basicString : Parser :=
litWithAntiquot "basicString" `Lake.Toml.basicString basicStringFn
def literalString : Parser :=
litWithAntiquot "literalString" `Lake.Toml.literalString literalStringFn
def mlBasicString : Parser :=
litWithAntiquot "mlBasicString" `Lake.Toml.mlBasicString mlBasicStringFn
def mlLiteralString : Parser :=
litWithAntiquot "mlLiteralString" `Lake.Toml.mlLiteralString mlLiteralStringFn
def quotedKey : Parser :=
basicString <|> literalString
def simpleKey : Parser := nodeWithAntiquot "simpleKey" `Lake.Toml.simpleKey (anonymous := true) $
unquotedKey <|> quotedKey
def key : Parser := nodeWithAntiquot "key" `Lake.Toml.key (anonymous := true) $ setExpected ["key"] $
sepBy1 simpleKey "." (trailingWs >> chAtom '.' >> trailingWs)
def stdTable : Parser := nodeWithAntiquot "stdTable" `Lake.Toml.stdTable $
atomic (chAtom '[' ["table"] >> notFollowedBy (chAtom '[') "'['") >>
trailingWs >> key >> trailingWs >> chAtom ']'
def arrayTable : Parser := nodeWithAntiquot "arrayTable" `Lake.Toml.arrayTable $
atomic (chAtom '[' ["table"] >> chAtom '[' ) >>
trailingWs >> key >> trailingWs >> chAtom ']' >> chAtom ']'
def table :=
stdTable <|> arrayTable
def keyvalCore (val : Parser) : Parser := nodeWithAntiquot "keyval" `Lake.Toml.keyval (anonymous := true) $
key >> trailingWs >> chAtom '=' >> trailingWs >> val
def expressionCore (val : Parser) : Parser :=
withAntiquot (mkAntiquot "expression" `Lake.Toml.expression (isPseudoKind := true)) $
keyvalCore val <|> table
def header : Parser :=
litWithAntiquot "header" `Lake.Toml.header skipFn trailingFn
def tomlCore (val : Parser) : Parser :=
nodeWithAntiquot "toml" `Lake.Toml.toml (anonymous := true) $
header >> sepByLinebreak (expressionCore val >> trailingSep)
def inlineTableCore (val : Parser) : Parser := nodeWithAntiquot "inlineTable" `Lake.Toml.inlineTable $
chAtom '{' ["inline-table"] (trailingFn := trailingFn) >>
sepBy (keyvalCore val >> trailingWs) "," (chAtom ',' (trailingFn := wsFn)) false >>
chAtom '}'
def arrayCore (val : Parser) : Parser := nodeWithAntiquot "array" `Lake.Toml.array $
chAtom '[' ["array"] (trailingFn := trailingFn) >>
sepBy (val >> trailingSep) "," (chAtom ',' (trailingFn := trailingFn)) true >>
chAtom ']'
def string : Parser :=
nodeWithAntiquot "string" `Lake.Toml.string $ setExpected ["string"] $
mlBasicString <|> basicString <|> mlLiteralString <|> literalString
protected def true : Parser :=
lit `Lake.Toml.true $ strFn "true"
protected def false : Parser :=
lit `Lake.Toml.false $ strFn "false"
def boolean : Parser :=
nodeWithAntiquot "boolean" `Lake.Toml.boolean $
Toml.true <|> Toml.false
def numeralAntiquot :=
mkAntiquot "float" `Lake.Toml.float (anonymous := false) <|>
mkAntiquot "decInt" `Lake.Toml.decInt (anonymous := false) <|>
mkAntiquot "binNum" `Lake.Toml.binNum (anonymous := false) <|>
mkAntiquot "octNum" `Lake.Toml.octNum (anonymous := false) <|>
mkAntiquot "hexNum" `Lake.Toml.hexNum (anonymous := false) <|>
mkAntiquot "dateTime" `Lake.Toml.dateTime (anonymous := false) <|>
mkAntiquot "numeral" `Lake.Toml.numeral (isPseudoKind := true)
/- A value starting with a numeral. Either a TOML date-time, float, or integer. -/
def numeral : Parser :=
withAntiquot numeralAntiquot $ dynamicNode numeralFn
def numeralOfKind (name : String) (kind : SyntaxNodeKind) : Parser :=
numeral >> setExpected [name] (checkStackTop (·.isOfKind kind) "illegal numeral kind")
def float : Parser :=
numeralOfKind "float" `Lake.Toml.float
def decInt : Parser :=
numeralOfKind "decimal integer" `Lake.Toml.decInt
def binNum : Parser :=
numeralOfKind "binary number" `Lake.Toml.binNum
def octNum : Parser :=
numeralOfKind "octal number" `Lake.Toml.octNum
def hexNum : Parser :=
numeralOfKind "hexadecimal number" `Lake.Toml.hexNum
def dateTime : Parser :=
numeralOfKind "date-time" `Lake.Toml.dateTime
def valCore (val : Parser) : Parser :=
string <|> boolean <|> numeral <|>
arrayCore val <|> inlineTableCore val
def val : Parser :=
recNodeWithAntiquot "val" `Lake.Toml.val valCore (anonymous := true)
def array : Parser :=
arrayCore val
def inlineTable : Parser :=
inlineTableCore val
def keyval : Parser :=
keyvalCore val
def expression : Parser :=
expressionCore val
@[run_parser_attribute_hooks] def toml : Parser :=
withCache `Lake.Toml.toml $ tomlCore val

34
src/lake/Lake/Toml/Load.lean Normal file
View file

@ -0,0 +1,34 @@
/-
Copyright (c) 2024 Mac Malone. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Mac Malone
-/
import Lake.Toml.Elab
import Lake.Util.Message
open Lean Parser
namespace Lake.Toml
/-- Load a TOML table from some input. -/
def loadToml (ictx : InputContext) : EIO MessageLog Table := do
let env ←
match (← mkEmptyEnvironment.toBaseIO) with
| .ok env => pure env
| .error e => throw <| MessageLog.empty.add <| mkMessageNoPos ictx <|
m!"failed to initialize TOML environment: {e}"
let s := toml.fn.run ictx { env, options := {} } {} (mkParserState ictx.input)
if let some errorMsg := s.errorMsg then
throw <| MessageLog.empty.add <| mkParserErrorMessage ictx s errorMsg
else if ictx.input.atEnd s.pos then
let act := elabToml ⟨s.stxStack.back⟩
match (← act.run {fileName := ictx.fileName, fileMap := ictx.fileMap} {env} |>.toBaseIO) with
| .ok (t, s) =>
if s.messages.hasErrors then
throw s.messages
else
return t
| .error e =>
throw <| MessageLog.empty.add <| mkExceptionMessage ictx e
else
throw <| MessageLog.empty.add <| mkParserErrorMessage ictx s {expected := ["end of input"]}

301
src/lake/Lake/Toml/ParserUtil.lean Normal file
View file

@ -0,0 +1,301 @@
/-
Copyright (c) 2024 Mac Malone. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Mac Malone
-/
import Lean.Parser
import Lean.PrettyPrinter.Formatter
/-!
# TOML Parser Utilities
Generic parser utilities used by Lake's TOML parser.
-/
namespace Lake.Toml
open Lean Parser PrettyPrinter Formatter
def isBinDigit (c : Char) : Bool :=
c == '0' || c == '1'
def isOctDigit (c : Char) : Bool :=
'0' ≤ c && c ≤ '7'
def isHexDigit (c : Char) : Bool :=
('0' ≤ c && c ≤ '9') || ('a' ≤ c && c ≤ 'f') || ('A' ≤ c && c ≤ 'F')
def skipFn : ParserFn := fun _ s => s
scoped instance : AndThen ParserFn where
andThen p q := fun c s => let s := p c s; if s.hasError then s else q () c s
/-- `ParserFn` combinator that runs `f` with the current position. -/
@[always_inline, inline] def usePosFn (f : String.Pos → ParserFn) : ParserFn :=
fun c s => f s.pos c s
/-- Match an arbitrary parser or do nothing. -/
def optFn (p : ParserFn) : ParserFn := fun c s =>
let iniSz := s.stackSize
let iniPos := s.pos
let s := p c s
if s.hasError && s.pos == iniPos then s.restore iniSz iniPos else s
/-- A sequence of `n` repetitions of a parser function. -/
@[inline] def repeatFn (n : Nat) (p : ParserFn) : ParserFn := fun c s =>
let rec @[specialize] loop
| 0, s => s
| n+1, s =>
let s := p c s
if s.hasError then s else loop n s
loop n s
def mkUnexpectedCharError (s : ParserState) (c : Char) (expected : List String := []) (pushMissing := true) : ParserState :=
s.mkUnexpectedError s!"unexpected '{c}'" expected pushMissing
@[inline] def satisfyFn (p : Char → Bool) (expected : List String := []) : ParserFn := fun c s =>
let i := s.pos
if h : c.input.atEnd i then
s.mkEOIError expected
else
let curr := c.input.get' i h
if p curr then
s.next' c.input i h
else
mkUnexpectedCharError s curr expected
def takeWhile1Fn (p : Char → Bool) (expected : List String := []) : ParserFn :=
satisfyFn p expected >> takeWhileFn p
/-- Consume a single digit (i.e., `Char.isDigit`). -/
def digitFn (expected : List String := ["digit"]) : ParserFn :=
satisfyFn Char.isDigit expected
/-- Consume a two digits (i.e., `Char.isDigit`). -/
def digitPairFn (expected := ["digit"]) : ParserFn :=
digitFn expected >> digitFn expected
/-- Consume a single matching character. -/
def chFn (c : Char) (expected : List String := [s!"'{c}'"]) : ParserFn :=
satisfyFn (fun d => d == c) expected
partial def strAuxFn (str : String) (expected : List String) (strPos : String.Pos) : ParserFn := fun c s =>
if h₁ : str.atEnd strPos then
s
else
let s := chFn (str.get' strPos h₁) expected c s
if s.hasError then s else strAuxFn str expected (str.next' strPos h₁) c s
/-- Consume a matching string atomically. -/
def strFn (str : String) (expected : List String := [s!"'{str}'"]) : ParserFn :=
atomicFn <| strAuxFn str expected 0
mutual
partial def sepByChar1AuxFn (p : Char → Bool) (sep : Char) (expected : List String := []) : ParserFn := fun c s =>
let i := s.pos
let input := c.input
if h : input.atEnd i then
s
else
let curr := input.get' i h
if p curr then
sepByChar1AuxFn p sep expected c (s.next' input i h)
else if curr == sep then
sepByChar1Fn p sep expected c (s.next' input i h)
else
s
partial def sepByChar1Fn (p : Char → Bool) (sep : Char) (expected : List String := []) : ParserFn := fun c s =>
let i := s.pos
let input := c.input
if h : input.atEnd i then
s
else
let curr := input.get' i h
let s := s.next' input i h
if p curr then
sepByChar1AuxFn p sep expected c s
else if curr == sep then
s.mkUnexpectedError s!"unexpected separator '{curr}'" expected
else
mkUnexpectedCharError s curr expected
end
/-- Push a new atom onto the syntax stack. -/
def pushAtom (startPos : String.Pos) (trailingFn := skipFn) : ParserFn := fun c s =>
let input := c.input
let stopPos := s.pos
let leading := mkEmptySubstringAt input startPos
let val := input.extract startPos stopPos
let s := trailingFn c s
let stopPos' := s.pos
let trailing := { str := input, startPos := stopPos, stopPos := stopPos' : Substring }
let atom := mkAtom (SourceInfo.original leading startPos trailing (startPos + val)) val
s.pushSyntax atom
/-- Match an arbitrary `ParserFn` and return the consumed String in a `Syntax.atom`. -/
def atomFn (p : ParserFn) (trailingFn := skipFn) : ParserFn := fun c s =>
let startPos := s.pos
let s := p c s
if s.hasError then s else
pushAtom startPos trailingFn c s
def atom (p : ParserFn) (trailingFn := skipFn) : Parser where
fn := atomFn p trailingFn
def getInfoExprPos? : SourceInfo → Option String.Pos
| SourceInfo.synthetic (pos := pos) .. => pos
| _ => none
def getSyntaxExprPos? : Syntax → Option String.Pos
| .node info _ _ => getInfoExprPos? info
| .atom info _ => getInfoExprPos? info
| .ident info _ _ _ => getInfoExprPos? info
| .missing => none
open Formatter Syntax.MonadTraverser in
@[combinator_formatter atom] def atom.formatter (_ _ : ParserFn) : Formatter := do
let stx ← getCur
let .atom info val := stx
| trace[PrettyPrinter.format.backtrack] "unexpected syntax '{format stx}', expected atom"
throwBacktrack
withMaybeTag (getSyntaxExprPos? stx) (pushToken info val)
goLeft
@[combinator_parenthesizer atom]
def atom.parenthesizer (_ _ : ParserFn) : Parenthesizer :=
Parenthesizer.visitToken
/-- Parse a single character as an atom. -/
def chAtom (c : Char) (expected := [s!"'{c}'"]) (trailingFn := skipFn) : Parser :=
atom (chFn c expected) trailingFn
@[combinator_formatter chAtom]
def chAtom.formatter (c : Char) (_ : List String) (_ : ParserFn) : Formatter :=
rawCh.formatter c
@[combinator_parenthesizer chAtom]
def chAtom.parenthesizer (_ : Char) (_ : List String) (_ : ParserFn) : Parenthesizer :=
Parenthesizer.visitToken
/-- Parse the trimmed string as an atom (but use the full string for formatting). -/
def strAtom (s : String) (expected := [s!"'{s}'"]) (trailingFn := skipFn) : Parser :=
atom (strFn s.trim expected) trailingFn
@[combinator_formatter strAtom]
def strAtom.formatter (s : String) (_ : List String) (_ : ParserFn) : Formatter :=
symbolNoAntiquot.formatter s
@[combinator_parenthesizer strAtom]
def strAtom.parenthesizer (_ : String) (_ : List String) (_ : ParserFn) : Parenthesizer :=
Parenthesizer.visitToken
/-- Push `(Syntax.node kind <new-atom>)` onto the syntax stack. -/
def pushLit (kind : SyntaxNodeKind) (startPos : String.Pos) (trailingFn := skipFn) : ParserFn := fun c s =>
let input := c.input
let stopPos := s.pos
let leading := mkEmptySubstringAt input startPos
let val := input.extract startPos stopPos
let s := trailingFn c s
let wsStopPos := s.pos
let trailing := { str := input, startPos := stopPos, stopPos := wsStopPos : Substring }
let info := SourceInfo.original leading startPos trailing stopPos
s.pushSyntax (Syntax.mkLit kind val info)
def litFn (kind : SyntaxNodeKind) (p : ParserFn) (trailingFn := skipFn) : ParserFn := fun c s =>
let iniPos := s.pos
let s := p c s
if s.hasError then s else
pushLit kind iniPos trailingFn c s
def lit (kind : SyntaxNodeKind) (p : ParserFn) (trailingFn := skipFn) : Parser where
fn := litFn kind p trailingFn
@[combinator_formatter lit]
def lit.formatter (kind : SyntaxNodeKind) (_ _ : ParserFn) : Formatter :=
visitAtom kind
@[combinator_parenthesizer lit]
def lit.parenthesizer (_ : SyntaxNodeKind) (_ _ : ParserFn) : Parenthesizer :=
Parenthesizer.visitToken
def litWithAntiquot (name : String) (kind : SyntaxNodeKind) (p : ParserFn) (trailingFn := skipFn) (anonymous := false) : Parser :=
withAntiquot (mkAntiquot name kind anonymous) $ lit kind p trailingFn
@[inline] def epsilon (fn : ParserFn) : Parser :=
{fn := fn, info := epsilonInfo}
@[combinator_formatter epsilon]
def epsilon.formatter (_ : ParserFn) : Formatter := pure ()
@[combinator_parenthesizer epsilon]
def epsilon.parenthesizer (_ : ParserFn) : Parenthesizer := pure ()
def SourceInfo.updateTrailing (trailing : Substring) : SourceInfo → SourceInfo
| SourceInfo.original leading pos _ endPos => SourceInfo.original leading pos trailing endPos
| info => info
partial def modifyTailInfo (f : SourceInfo → SourceInfo) : (stx : Syntax) → Syntax
| .atom info val => .atom (f info) val
| .ident info rawVal val pre => .ident (f info) rawVal val pre
| .node info k args =>
.node info k <| args.modify (args.size - 1) (modifyTailInfo f)
| s => s
def extendTrailingFn (p : ParserFn) : ParserFn := fun c s =>
let s := p c s
let stopPos := s.pos
let tail := s.stxStack.back
let s := s.popSyntax -- try for linearity
let tail := modifyTailInfo (stx := tail) fun
| .original leading pos trailing endPos =>
.original leading pos {trailing with stopPos} endPos
| info => info
s.pushSyntax tail
def trailing (p : ParserFn) : Parser :=
epsilon (extendTrailingFn p)
def dynamicNode (p : ParserFn) : Parser where
fn := p
@[combinator_formatter dynamicNode]
def dynamicNode.formatter (_ : ParserFn) : Formatter := do
formatterForKind (← Syntax.MonadTraverser.getCur).getKind
@[combinator_parenthesizer dynamicNode]
def dynamicNode.parenthesizer (_ : ParserFn) : Parenthesizer := do
Parenthesizer.parenthesizerForKind (← Syntax.MonadTraverser.getCur).getKind
partial def recNodeFn (f : Parser → Parser) : ParserFn :=
f (dynamicNode (recNodeFn f)) |>.fn
/--
`Parser → Parser` hidden by an `abbrev`.
Prevents the formatter/parenthesizer generator from transforming it.
-/
abbrev ParserMapFn := Parser → Parser
def recNode (f : ParserMapFn) : Parser :=
dynamicNode (recNodeFn f)
def recNodeWithAntiquot (name : String) (kind : SyntaxNodeKind) (f : ParserMapFn) (anonymous := false) : Parser :=
withCache kind $ withAntiquot (mkAntiquot name kind anonymous true) $ recNode go
where
go p := withCache kind $ withAntiquot (mkAntiquot name kind anonymous true) $ f p
@[inline] def sepByLinebreak (p : Parser) (allowTrailingLinebreak := true) : Parser :=
let p := withAntiquotSpliceAndSuffix `sepBy p (symbol "*")
sepByNoAntiquot p (checkLinebreakBefore >> pushNone) allowTrailingLinebreak
@[inline] def sepBy1Linebreak (p : Parser) (allowTrailingLinebreak := true) : Parser :=
let p := withAntiquotSpliceAndSuffix `sepBy p (symbol "*")
sepBy1NoAntiquot p (checkLinebreakBefore >> pushNone) allowTrailingLinebreak
def skipInsideQuotFn (p : ParserFn) : ParserFn := fun c s =>
if c.quotDepth > 0 then s else p c s
@[run_parser_attribute_hooks] def skipInsideQuot (p : Parser) : Parser :=
withFn skipInsideQuotFn p

28
src/lake/Lake/Util/FilePath.lean Normal file
View file

@ -0,0 +1,28 @@
/-
Copyright (c) 2024 Mac Malone. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Mac Malone
-/
import Lean.ToExpr
import Lean.Data.Json
open System Lean
namespace Lake
/--
Convert a relative file path to a platform-independent string.
Uses `/` as the path separator, even on Windows.
-/
def mkRelPathString (path : FilePath) : String :=
if System.Platform.isWindows then
path.toString.map fun c => if c = '\\' then '/' else c
else
path.toString
scoped instance : ToJson FilePath where
toJson path := toJson <| mkRelPathString path
scoped instance : ToExpr FilePath where
toExpr p := mkApp (mkConst ``System.FilePath.mk) (toExpr p.toString)
toTypeExpr := mkConst ``System.FilePath

65
src/lake/Lake/Util/Message.lean Normal file
View file

@ -0,0 +1,65 @@
/-
Copyright (c) 2024 Mac Malone. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Mac Malone
-/
import Lean.Message
import Lean.Exception
import Lean.Parser.Basic
open Lean Parser
namespace Lake
def mkParserErrorMessage (ictx : InputContext) (s : ParserState) (e : Parser.Error) : Message where
fileName := ictx.fileName
pos := ictx.fileMap.toPosition s.pos
endPos := none
keepFullRange := true
data := toString e
def mkExceptionMessage (ictx : InputContext) (e : Exception) : Message where
fileName := ictx.fileName
pos := ictx.fileMap.toPosition <| e.getRef.getPos?.getD 0
endPos := ictx.fileMap.toPosition <$> e.getRef.getTailPos?
data := e.toMessageData
def mkMessageNoPos (ictx : InputContext) (data : MessageData) (severity := MessageSeverity.error) : Message where
fileName := ictx.fileName
pos := ictx.fileMap.toPosition 0
endPos := none
severity := severity
data := data
def mkMessageStringCore
(severity : MessageSeverity)
(fileName caption body : String)
(pos : Position) (endPos? : Option Position := none)
(infoWithPos := false)
: String := Id.run do
let mut str := body
unless caption == "" do
str := caption ++ ":\n" ++ str
match severity with
| .information =>
if infoWithPos then
str := mkErrorStringWithPos fileName pos (endPos := endPos?) "info: " ++ str
| .warning =>
str := mkErrorStringWithPos fileName pos (endPos := endPos?) "warning: " ++ str
| .error =>
str := mkErrorStringWithPos fileName pos (endPos := endPos?) "error: " ++ str
if str.isEmpty || str.back != '\n' then
str := str ++ "\n"
return str
def mkMessageString (msg : Message) (includeEndPos := false) (infoWithPos := false) : BaseIO String := do
let endPos? := if includeEndPos then msg.endPos else none
match (← msg.data.toString.toBaseIO) with
| .ok s =>
return mkMessageStringCore msg.severity msg.fileName msg.caption s msg.pos endPos? infoWithPos
| .error e =>
return mkMessageStringCore .error msg.fileName msg.caption (toString e) msg.pos endPos? infoWithPos
def mkMessageLogString (log : MessageLog) : BaseIO String :=
log.toList.foldlM (init := "") fun s m => do
return s ++ (← mkMessageString m (infoWithPos := true))

24
src/lake/Lake/Util/Newline.lean Normal file
View file

@ -0,0 +1,24 @@
/-
Copyright (c) 2023 Mario Carneiro. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Mario Carneiro
-/
namespace Lake
/-- 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'

5
src/lake/Lake/Util/RBArray.lean
View file

@ -66,3 +66,8 @@ def insert (self : RBArray α β cmp) (a : α) (b : β) : RBArray α β cmp :=
self.toArray.forIn init f
instance : ForIn m (RBArray α β cmp) β := ⟨RBArray.forIn⟩
end RBArray
@[inline] def mkRBArray (f : β → α) (vs : Array β) : RBArray α β cmp :=
vs.foldl (init := RBArray.mkEmpty vs.size) fun m v => m.insert (f v) v

44
src/lake/README.md
View file

@ -36,7 +36,7 @@ Lake is part of the [lean4](https://github.com/leanprover/lean4) repository and
## Creating and Building a Package
To create a new package, either run `lake init <package-name> [<template>]` to setup the package in the current directory or `lake new <package-name> [<template>]` to create it in a new directory. For example, we could create the package `hello` like so:
To create a new package, either run `lake init` to setup the package in the current directory or `lake new` to create it in a new directory. For example, we could create the package `hello` like so:
```
$ mkdir hello
@ -115,7 +115,22 @@ $ ./.lake/build/bin/hello
Hello, world!
```
Examples of different package configurations can be found in the [`examples`](examples) folder of this repository. You can also specified a particular configuration file template when using `lake init` or `lake new` to control what files Lake creates. See `lake help init` or `lake help new` for details.
Examples of different package configurations can be found in the [`examples`](examples) folder of this repository. You can also pass a package template tp `lake init` or `lake new` to control what files Lake creates. For example, instead of using a Lean configuration file for this package, one could produce a TOML version via `lake new hello .toml`.
**lakefile.toml**
```toml
name = "hello"
defaultTargets = ["hello"]
[[lean_lib]]
name = "Hello"
[[lean_exe]]
name = "hello"
root = "Main"
```
See `lake help init` or `lake help new` for more details on other template options.
## Glossary of Terms
@ -195,6 +210,12 @@ lean_lib «target-name» where
-- configuration options go here
```
```toml
[[lean_lib]]
name = "«target-name»"
# more configuration options go here
```
**Configuration Options**
* `srcDir`: The subdirectory of the package's source directory containing the library's source files. Defaults to the package's `srcDir`. (This will be passed to `lean` as the `-R` option.)
@ -217,6 +238,12 @@ lean_exe «target-name» where
-- configuration options go here
```
```toml
[[lean_exe]]
name = "«target-name»"
# more configuration options go here
```
**Configuration Options**
* `srcDir`: The subdirectory of the package's source directory containing the executable's source file. Defaults to the package's `srcDir`. (This will be passed to `lean` as the `-R` option.)
@ -304,6 +331,19 @@ The first form adds a local dependency and the second form adds a Git dependency
Both forms also support an optional `with` clause to specify arguments to pass to the dependency's package configuration (i.e., same as `args` in a `lake build -- <args...>` invocation). The elements of both the `from` and `with` clauses are proper terms so normal computation is supported within them (though parentheses made be required to disambiguate the syntax).
To `require` a package in a TOML configuration, the equivalent syntax is:
```toml
[[require]]
path = "path/to/local/package"
options = {}
[[require]]
git = "url.git"
rev = "rev"
subDir = "optional/path-to/dir-with-pkg"
```
## GitHub Release Builds
Lake supports uploading and downloading build artifacts (i.e., the archived build directory) to/from the GitHub releases of packages. This enables end users to fetch pre-built artifacts from the cloud without needed to rebuild the package from the source themselves.

11
src/lake/examples/bootstrap/lakefile.toml Normal file
View file

@ -0,0 +1,11 @@
name = "lake"
srcDir = "../.."
defaultTargets = ["lake"]
[[lean_lib]]
name = "Lake"
[[lean_exe]]
name = "lake"
root = "Lake.Main"
supportInterpreter = true

13
src/lake/examples/deps/bar/lakefile.toml Normal file
View file

@ -0,0 +1,13 @@
name = "bar"
defaultTargets = ["bar"]
[[require]]
name = "foo"
path = "../foo"
[[lean_lib]]
name = "Bar"
[[lean_exe]]
name = "bar"
root = "Main"

17
src/lake/examples/deps/foo/lakefile.toml Normal file
View file

@ -0,0 +1,17 @@
name = "foo"
defaultTargets = ["foo"]
[[require]]
name = "a"
path = "../a"
[[require]]
name = "b"
path = "../b"
[[lean_lib]]
name = "Foo"
[[lean_exe]]
name = "foo"
root = "Main"

8
src/lake/examples/deps/test.sh
View file

@ -25,3 +25,11 @@ test -d foo/.lake/build
$LAKE -d foo clean
test ! -d root/.lake/build
test ! -d foo/.lake/build
./clean.sh
$LAKE -d bar -f lakefile.toml build --update
$LAKE -d foo -f lakefile.toml build --update
./foo/.lake/build/bin/foo
./bar/.lake/build/bin/bar

9
src/lake/examples/hello/lakefile.toml Normal file
View file

@ -0,0 +1,9 @@
name = "hello"
defaultTargets = ["hello"]
[[lean_lib]]
name = "Hello"
[[lean_exe]]
name = "hello"
root = "Main"

6
src/lake/examples/hello/test.sh
View file

@ -11,3 +11,9 @@ $LAKE exe hello Bob Bill
# Tests that build produces a manifest if there is none.
# Related: https://github.com/leanprover/lean4/issues/2549
test -f lake-manifest.json
./clean.sh
$LAKE -f lakefile.toml exe hello
$LAKE -f lakefile.toml exe hello Bob Bill
.lake/build/bin/hello

3
src/lake/examples/precompile/bar/lakefile.lean
View file

@ -1,9 +1,8 @@
import Lake
open Lake DSL
package bar {
package bar where
precompileModules := false
}
require foo from "../foo"

10
src/lake/examples/precompile/bar/lakefile.toml Normal file
View file

@ -0,0 +1,10 @@
name = "bar"
precompileModules = false
defaultTargets = ["Bar"]
[[require]]
name = "foo"
path = "../foo"
[[lean_lib]]
name = "Bar"

3
src/lake/examples/precompile/foo/lakefile.lean
View file

@ -1,9 +1,8 @@
import Lake
open Lake DSL
package foo {
package foo where
precompileModules := true
}
@[default_target]
lean_lib Foo

6
src/lake/examples/precompile/foo/lakefile.toml Normal file
View file

@ -0,0 +1,6 @@
name = "foo"
precompileModules = true
defaultTargets = ["Foo"]
[[lean_lib]]
name = "Foo"

7
src/lake/examples/precompile/test.sh
View file

@ -4,5 +4,10 @@ LAKE=${LAKE:-../../.lake/build/bin/lake}
./clean.sh
$LAKE -d bar update
$LAKE -d bar build # tests #83
$LAKE -d bar build # tests lake#83
$LAKE -d foo build
./clean.sh
$LAKE -d bar -f lakefile.toml update
$LAKE -d bar -f lakefile.toml build
$LAKE -d foo -f lakefile.toml build

6
src/lake/tests/globs/lakefile.lean
View file

@ -4,10 +4,8 @@ open Lake DSL
package test
@[default_target]
lean_lib TBA where
globs := #[.andSubmodules `TBA]
globs := `TBA.*
@[default_target]
lean_lib Test where
globs := #[.submodules `Test]
globs := #[`Test.+]

9
src/lake/tests/globs/lakefile.toml Normal file
View file

@ -0,0 +1,9 @@
name = 'test'
[[lean_lib]]
name = 'TBA'
globs = 'TBA.*'
[[lean_lib]]
name = 'Test'
globs = ['Test.+']

10
src/lake/tests/globs/test.sh
View file

@ -12,6 +12,11 @@ $LAKE build TBA
test -f .lake/build/lib/TBA.olean
test -f .lake/build/lib/TBA/Eulerian.olean
test -f .lake/build/lib/TBA/Eulerian/A.olean
rm -rf .lake
$LAKE -f lakefile.toml build TBA
test -f .lake/build/lib/TBA.olean
test -f .lake/build/lib/TBA/Eulerian.olean
test -f .lake/build/lib/TBA/Eulerian/A.olean
# test that globs capture modules with non-Lean names
# see https://github.com/leanprover/lake/issues/174
@ -22,4 +27,7 @@ test -f .lake/build/lib/TBA/Eulerian/A.olean
$LAKE build Test
test -f .lake/build/lib/Test/1.olean
test -f .lake/build/lib/Test/Subtest/1.olean
rm -rf .lake
$LAKE -f lakefile.toml build Test
test -f .lake/build/lib/Test/1.olean
test -f .lake/build/lib/Test/Subtest/1.olean

55
src/lake/tests/init/test.sh
View file

@ -13,10 +13,12 @@ fi
LAKE1=${LAKE:-../../../.lake/build/bin/lake}
LAKE=${LAKE:-../../.lake/build/bin/lake}
# Test `new` and `init` with bad template (should error)
# Test `new` and `init` with bad template/langauge (should error)
($LAKE new foo bar 2>&1 && false || true) | grep "unknown package template"
($LAKE new foo bar 2>&1 && false || true) | grep "unknown package template"
($LAKE new foo .baz 2>&1 && false || true) | grep "unknown configuration language"
($LAKE init foo bar 2>&1 && false || true) | grep "unknown package template"
($LAKE init foo std.baz 2>&1 && false || true) | grep "unknown configuration language"
# Test package name validation (should error)
# https://github.com/leanprover/lean4/issues/2637
@ -34,13 +36,36 @@ for cmd in new init; do
($LAKE $cmd main 2>&1 && false || true) | grep "reserved package name"
done
# Test `init .`
# Test default (std) template
mkdir hello
pushd hello
$LAKE1 init .
$LAKE1 exe hello
popd
$LAKE new hello
$LAKE -d hello exe hello
test -f hello/.lake/build/lib/Hello.olean
rm -rf hello
$LAKE new hello .toml
$LAKE -d hello exe hello
test -f hello/.lake/build/lib/Hello.olean
rm -rf hello
# Test exe template
$LAKE new hello exe
$LAKE -d hello exe hello
rm -rf hello
$LAKE new hello exe.toml
$LAKE -d hello exe hello
rm -rf hello
# Test lib template
$LAKE new hello lib
$LAKE -d hello build Hello
test -f hello/.lake/build/lib/Hello.olean
rm -rf hello
$LAKE new hello lib.toml
$LAKE -d hello build Hello
test -f hello/.lake/build/lib/Hello.olean
rm -rf hello
# Test math template
@ -49,6 +74,20 @@ $LAKE new qed math
sed_i '/^require.*/{N;d;}' qed/lakefile.lean
$LAKE -d qed build Qed
test -f qed/.lake/build/lib/Qed.olean
rm -rf qed
$LAKE new qed math.toml
# Remove the require, since we do not wish to download mathlib during tests
sed_i '/^\[\[require\]\]/{N;N;N;d;}' qed/lakefile.toml
$LAKE -d qed build Qed
test -f qed/.lake/build/lib/Qed.olean
# Test `init .`
mkdir hello
pushd hello
$LAKE1 init .
$LAKE1 exe hello
popd
# Test creating packages with uppercase names
# https://github.com/leanprover/lean4/issues/2540

26
src/lake/tests/toml/README.md Normal file
View file

@ -0,0 +1,26 @@
Test cases are taken from https://github.com/toml-lang/toml-test, which
is licensed under the MIT license. The license is copied below.
```
The MIT License (MIT)
Copyright (c) 2018 TOML authors
Permission is hereby granted, free of charge, to any person obtaining a copy
of this software and associated documentation files (the "Software"), to deal
in the Software without restriction, including without limitation the rights
to use, copy, modify, merge, publish, distribute, sublicense, and/or sell
copies of the Software, and to permit persons to whom the Software is
furnished to do so, subject to the following conditions:
The above copyright notice and this permission notice shall be included in
all copies or substantial portions of the Software.
THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE
AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER
LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM,
OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN
THE SOFTWARE.
```

217
src/lake/tests/toml/Test.lean Normal file
View file

@ -0,0 +1,217 @@
/-
Copyright (c) 2024 Mac Malone. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Mac Malone
-/
import Lake.Toml
import Lake.Util.Message
import Lake.Util.Newline
/-!
## TOML Test Runner
Tests Lake's TOML implementation against the version of the [toml-test][1]
compliance suite stored in `tests` (currently, suite v1.4.0 for TOML v1.0.0).
[1]: https://github.com/toml-lang/toml-test
-/
open Lake Toml
open Lean Parser System
inductive TomlOutcome where
| pass (t : Table)
| fail (log : MessageLog)
| error (e : IO.Error)
@[inline] def Fin.allM [Monad m] (n) (f : Fin n → m Bool) : m Bool :=
loop 0
where
loop (i : Nat) : m Bool := do
if h : i < n then
if (← f ⟨i, h⟩) then loop (i+1) else pure false
else
pure true
termination_by n - i
@[inline] def Fin.all (n) (f : Fin n → Bool) : Bool :=
Id.run <| allM n f
def bytesBEq (a b : ByteArray) : Bool :=
if h_size : a.size = b.size then
Fin.all a.size fun i => a[i] = b[i]'(h_size ▸ i.isLt)
else
false
def String.fromUTF8 (bytes : ByteArray) : String :=
String.fromUTF8Unchecked bytes |>.map id
@[inline] def String.fromUTF8? (bytes : ByteArray) : Option String :=
let s := String.fromUTF8 bytes
if bytesBEq s.toUTF8 bytes then some s else none
nonrec def loadToml (tomlFile : FilePath) : BaseIO TomlOutcome := do
let fileName := tomlFile.fileName.getD tomlFile.toString
let input ←
match (← IO.FS.readBinFile tomlFile |>.toBaseIO) with
| .ok bytes =>
if let some input := String.fromUTF8? bytes then
pure (crlf2lf input)
else
return .fail <| MessageLog.empty.add
{fileName, pos := ⟨1,0⟩, data := m!"file contains invalid characters"}
| .error e => return .error e
let ictx := mkInputContext input fileName
match (← loadToml ictx |>.toBaseIO) with
| .ok table => return .pass table
| .error log => return .fail log
inductive TestOutcome
| skip
| pass (s : String)
| fail (s : String)
| error (e : String)
def testInvalid (tomlFile : FilePath) : BaseIO TestOutcome := do
match (← loadToml tomlFile) with
| .pass t => return .fail (ppTable t)
| .fail l => return .pass (← mkMessageLogString l)
| .error e => return .error (toString e)
@[inline] def Fin.forM [Monad m] (n) (f : Fin n → m Unit) : m Unit :=
loop 0
where
loop (i : Nat) : m Unit := do
if h : i < n then let a ← f ⟨i, h⟩; loop (i+1) else pure ()
termination_by n - i
local instance [Monad m] : ForIn m (RBNode α β) ((a : α) × β a) where
forIn t init f := t.forIn init (fun a b acc => f ⟨a, b⟩ acc)
def expectBEq [BEq α] [ToString α] (actual expected : α) : Except String Unit := do
unless actual == expected do
throw s!"expected '{expected}', got '{actual}'"
def expectPrimitive (actualTy : String) (expected : Json) : Except String String := do
let .ok expected := expected.getObj?
| throw s!"expected non-primitive, got '{actualTy}'"
let some ty := expected.find compare "type"
| throw s!"expected non-primitive, got '{actualTy}'"
let some val := expected.find compare "value"
| throw s!"expected non-primitive, got '{actualTy}'"
let .ok val := val.getStr?
| throw s!"expected non-primitive, got '{actualTy}'"
unless actualTy == ty do
throw s!"expected value of type '{ty}', got '{actualTy}'"
return val
mutual
partial def expectValue (actual : Value) (expected : Json) : Except String Unit := do
match actual with
| .boolean _ b => expectBEq (toString b) (← expectPrimitive "bool" expected)
| .string _ s => expectBEq s (← expectPrimitive "string" expected)
| .integer _ n => expectBEq (toString n) (← expectPrimitive "integer" expected)
| .float _ actN =>
let expected ← expectPrimitive "float" expected
if expected.toLower == "nan" then
unless actN.isNaN do
throw s!"expected '{expected}', got '{actN}'"
else
let (sign, e) := decodeSign expected
if e.toLower == "inf" then
unless actN.isInf && sign == (actN < 0) do
throw s!"expected '{e}', got '{actN}'"
else
let some flt :=
(Nat.toFloat <$> e.toNat?) <|>
(Syntax.decodeScientificLitVal? e |>.map fun (m,s,e) => .ofScientific m s e)
| throw s!"failed to parse expected float value: {e}"
expectBEq actN <| if sign then -flt else flt
| .dateTime _ dt =>
match dt with
| .offsetDateTime _ _ _ => expectBEq (toString dt) (← expectPrimitive "datetime" expected)
| .localDateTime .. => expectBEq (toString dt) (← expectPrimitive "datetime-local" expected)
| .localDate d => expectBEq (toString d) (← expectPrimitive "date-local" expected)
| .localTime t => expectBEq (toString t) (← expectPrimitive "time-local" expected)
| .array _ actVs =>
let .ok expVs := expected.getArr?
| throw "expected non-array, got array"
if h_size : actVs.size = expVs.size then
Fin.forM actVs.size fun i => expectValue actVs[i] (expVs[i]'(h_size ▸ i.isLt))
else
throw s!"expected array of size {expVs.size}, got {actVs.size}:\n{actual}"
| .table _ t => expectTable t expected
partial def expectTable (actual : Table) (expected : Json) : Except String Unit := do
let .ok expected := expected.getObj?
| throw "expected non-table, got table"
if actual.size != expected.size then
throw s!"expected table of size {expected.size}, got {actual.size}:\n{ppTable actual}"
for ⟨k,expV⟩ in expected do
let some actV := actual.find? (Name.mkSimple k)
| throw s!"expected key '{k}'"
try expectValue actV expV catch e => throw s!"{k}: {e}"
end
def expectJson (actual expected : Json) : TestOutcome :=
let s := actual.pretty ++ "\n"
if actual == expected then .pass s else .fail s
def testValid (tomlFile : FilePath) : BaseIO TestOutcome := do
-- Tests skipped due to bugs in Lean's JSON parser
-- TODO: Fix JSON parser (high-low unicode escape pairs)
let normPath := tomlFile.toString.map fun c => if c = '\\' then '/' else c
for testPath in ["string/quoted-unicode.toml", "key/quoted-unicode.toml"] do
if normPath.endsWith testPath then return .skip
match (← loadToml tomlFile) with
| .pass t =>
match (← IO.FS.readFile (tomlFile.withExtension "json") |>.toBaseIO) with
| .ok contents =>
match Json.parse contents with
| .ok j =>
match expectTable t j with
| .ok _ => return .pass <| ppTable t
| .error e => return .fail <| e.trimRight ++ "\n"
| .error e => return .error s!"invalid JSON: {e}"
| .error e => return .error (toString e)
| .fail l => return .fail (← mkMessageLogString l)
| .error e => return .error (toString e)
def walkDir (root : FilePath) (ext : String := "toml") : IO (Array FilePath) := do
(← root.walkDir).filterM fun path => do
return path.extension == some ext && !(← path.isDir)
def main : IO UInt32 := do
-- Detect Tests
let invalidTestFiles ← walkDir <| FilePath.mk "tests" / "invalid"
let validTestFiles ← walkDir <| FilePath.mk "tests" / "valid"
let numTests := invalidTestFiles.size + validTestFiles.size
let outcomes := Array.mkEmpty numTests
-- Run Tests
let outcomes ← invalidTestFiles.foldlM (init := outcomes) fun outcomes path => do
return outcomes.push (← IO.FS.realPath path, ← testInvalid path)
let outcomes ← validTestFiles.foldlM (init := outcomes) fun outcomes path => do
return outcomes.push (← IO.FS.realPath path, ← testValid path)
-- Print Results
let showPassedTests := false
let showOutputOnFail := true
let mut skipped := 0; let mut failed := 0; let mut errored := 0
for (testName, outcome) in outcomes do
match outcome with
| .skip =>
skipped := skipped + 1
| .pass s =>
if showPassedTests then
IO.print s!"{testName} passed:\n{s}"
| .fail s =>
failed := failed + 1
if showOutputOnFail && !s.isEmpty then
IO.print s!"{testName} failed:\n{s}"
else
IO.print s!"{testName} failed\n"
| .error s => errored := errored + 1; IO.print s!"{testName} errored:\n{s}\n"
let percent := (numTests - skipped - failed - errored) * 100 / numTests
IO.println s!"{percent}% of tests passed, {failed} failed, {errored} errored, {skipped} skipped out of {numTests}"
return if failed > 0 || errored > 0 then 1 else 0

12
src/lake/tests/toml/fetch-tests.sh Executable file
View file

@ -0,0 +1,12 @@
#!/usr/bin/env bash
set -euo pipefail
git clone https://github.com/toml-lang/toml-test toml-test --depth 1 --branch v1.4.0
TOML_VER=${1:-1.0.0}
echo "Copying tests for TOML v$TOML_VER..."
while read t; do
echo "$t"
mkdir -p tests/"$(dirname "$t")"
cp -r "toml-test/tests/$t" tests/"$t"
done < "toml-test/tests/files-toml-$TOML_VER"
rm -rf toml-test

5
src/lake/tests/toml/test.sh Executable file
View file

@ -0,0 +1,5 @@
#!/usr/bin/env bash
set -euo pipefail
LAKE=${LAKE:-../../.lake/build/bin/lake}
$LAKE -d ../.. build Lake.Toml
$LAKE env lean --run Test.lean

1
src/lake/tests/toml/tests/invalid/array/double-comma-1.toml Normal file
View file

@ -0,0 +1 @@
array = [1,,2]

2
src/lake/tests/toml/tests/invalid/array/double-comma-2.toml Normal file
View file

@ -0,0 +1,2 @@
array = [1,2,,]

3
src/lake/tests/toml/tests/invalid/array/extend-defined-aot.toml Normal file
View file

@ -0,0 +1,3 @@
[[tab.arr]]
[tab]
arr.val1=1

6
src/lake/tests/toml/tests/invalid/array/extending-table.toml Normal file
View file

@ -0,0 +1,6 @@
a = [{ b = 1 }]
# Cannot extend tables within static arrays
# https://github.com/toml-lang/toml/issues/908
[a.c]
foo = 1

1
src/lake/tests/toml/tests/invalid/array/missing-separator-1.toml Normal file
View file

@ -0,0 +1 @@
arrr = [true false]

1
src/lake/tests/toml/tests/invalid/array/missing-separator-2.toml Normal file
View file

@ -0,0 +1 @@
wrong = [ 1 2 3 ]

1
src/lake/tests/toml/tests/invalid/array/missing-separator.toml Normal file
View file

@ -0,0 +1 @@
wrong = [ 1 2 3 ]

1
src/lake/tests/toml/tests/invalid/array/no-close-1.toml Normal file
View file

@ -0,0 +1 @@
no-close-1 = [ 1, 2, 3

1
src/lake/tests/toml/tests/invalid/array/no-close-2.toml Normal file
View file

@ -0,0 +1 @@
x = [42 #

1
src/lake/tests/toml/tests/invalid/array/no-close-3.toml Normal file
View file

@ -0,0 +1 @@
no-close-3 = [42 #]

1
src/lake/tests/toml/tests/invalid/array/no-close-4.toml Normal file
View file

@ -0,0 +1 @@
no-close-4 = [{ key = 42

1
src/lake/tests/toml/tests/invalid/array/no-close-5.toml Normal file
View file

@ -0,0 +1 @@
no-close-5 = [{ key = 42}

1
src/lake/tests/toml/tests/invalid/array/no-close-6.toml Normal file
View file

@ -0,0 +1 @@
no-close-6 = [{ key = 42 #}]

1
src/lake/tests/toml/tests/invalid/array/no-close-7.toml Normal file
View file

@ -0,0 +1 @@
no-close-7 = [{ key = 42} #]

1
src/lake/tests/toml/tests/invalid/array/no-close-8.toml Normal file
View file

@ -0,0 +1 @@
no-close-8 = [

1
src/lake/tests/toml/tests/invalid/array/no-close-table-1.toml Normal file
View file

@ -0,0 +1 @@
x = [{ key = 42

1
src/lake/tests/toml/tests/invalid/array/no-close-table-2.toml Normal file
View file

@ -0,0 +1 @@
x = [{ key = 42 #

1
src/lake/tests/toml/tests/invalid/array/no-close-table.toml Normal file
View file

@ -0,0 +1 @@
x = [{ key = 42

1
src/lake/tests/toml/tests/invalid/array/no-close.toml Normal file
View file

@ -0,0 +1 @@
long_array = [ 1, 2, 3

1
src/lake/tests/toml/tests/invalid/array/no-comma-1.toml Normal file
View file

@ -0,0 +1 @@
no-comma-1 = [true false]

1
src/lake/tests/toml/tests/invalid/array/no-comma-2.toml Normal file
View file

@ -0,0 +1 @@
no-comma-2 = [ 1 2 3 ]

1
src/lake/tests/toml/tests/invalid/array/no-comma-3.toml Normal file
View file

@ -0,0 +1 @@
no-comma-3 = [ 1 #,]

1
src/lake/tests/toml/tests/invalid/array/only-comma-1.toml Normal file
View file

@ -0,0 +1 @@
only-comma-1 = [,]

1
src/lake/tests/toml/tests/invalid/array/only-comma-2.toml Normal file
View file

@ -0,0 +1 @@
only-comma-2 = [,,]

4
src/lake/tests/toml/tests/invalid/array/tables-1.toml Normal file
View file

@ -0,0 +1,4 @@
# INVALID TOML DOC
fruit = []
[[fruit]] # Not allowed

10
src/lake/tests/toml/tests/invalid/array/tables-2.toml Normal file
View file

@ -0,0 +1,10 @@
# INVALID TOML DOC
[[fruit]]
name = "apple"
[[fruit.variety]]
name = "red delicious"
# This table conflicts with the previous table
[fruit.variety]
name = "granny smith"

4
src/lake/tests/toml/tests/invalid/array/text-after-array-entries.toml Normal file
View file

@ -0,0 +1,4 @@
array = [
"Is there life after an array separator?", No
"Entry"
]

4
src/lake/tests/toml/tests/invalid/array/text-before-array-separator.toml Normal file
View file

@ -0,0 +1,4 @@
array = [
"Is there life before an array separator?" No,
"Entry"
]

5
src/lake/tests/toml/tests/invalid/array/text-in-array.toml Normal file
View file

@ -0,0 +1,5 @@
array = [
"Entry 1",
I don't belong,
"Entry 2",
]

1
src/lake/tests/toml/tests/invalid/bool/almost-false-with-extra.toml Normal file
View file

@ -0,0 +1 @@
a = falsify

1
src/lake/tests/toml/tests/invalid/bool/almost-false.toml Normal file
View file

@ -0,0 +1 @@
a = fals

1
src/lake/tests/toml/tests/invalid/bool/almost-true-with-extra.toml Normal file
View file

@ -0,0 +1 @@
a = truthy

1
src/lake/tests/toml/tests/invalid/bool/almost-true.toml Normal file
View file

@ -0,0 +1 @@
a = tru

1
src/lake/tests/toml/tests/invalid/bool/capitalized-false.toml Normal file
View file

@ -0,0 +1 @@
capitalized-false = False

Some files were not shown because too many files have changed in this diff Show more