Add files using upload-large-folder tool

backend/core/leanprover--lean4---v4.22.0/src/lean/lake/Lake/DSL/Key.lean

@@ -0,0 +1,53 @@
+/-
+Copyright (c) 2025 Mac Malone. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Mac Malone
+-/
+prelude
+import Lake.Build.Key
+import Lake.DSL.Syntax
+
+/-! # DSL for Build Key
+Notation for specifying build keys in a package.
+-/
+
+open Lean
+
+namespace Lake.DSL
+
+private def expandFacets (tgt : Term) (facets : Array Ident) : MacroM Term := do
+  let facetLits := facets.map fun facet => Name.quoteFrom facet facet.getId
+  facetLits.foldlM (init := tgt) fun tgt lit => `(BuildKey.facet $tgt $lit)
+
+private def expandPackageTargetLit
+  (pkg : Term) (stx : TSyntax ``packageTargetLit)
+: MacroM Term := withRef stx do
+  let `(packageTargetLit|$[+%$mod?]?$tgt) := stx
+    | Macro.throwError "ill-formed package target literal"
+  let tgtName :=
+    if mod?.isSome then
+      tgt.getId ++ PartialBuildKey.moduleTargetIndicator
+    else
+      tgt.getId
+  let tgtLit := Name.quoteFrom tgt tgtName
+  `(BuildKey.packageTarget $pkg $tgtLit)
+
+macro_rules
+| `(`+%$tk$mod$[:$facets]*) => withRef tk do
+  let modLit := Name.quoteFrom mod mod.getId
+  let tgt ← `(BuildKey.module $modLit)
+  let key ← expandFacets tgt facets
+  `(PartialBuildKey.mk $key)
+| `(`@%$tk$(pkg?)?$[/$tgt?]?$[:$facets]*) => withRef tk do
+  let pkgLit :=
+    if let some pkg := pkg? then
+      Name.quoteFrom pkg pkg.getId
+    else
+      Name.quoteFrom tk Name.anonymous
+  let tgt ←
+    if let some tgt := tgt? then
+      expandPackageTargetLit pkgLit tgt
+    else
+      `(BuildKey.package $pkgLit)
+  let key ← expandFacets tgt facets
+  `(PartialBuildKey.mk $key)

backend/core/leanprover--lean4---v4.22.0/src/lean/lake/Lake/DSL/Meta.lean

@@ -0,0 +1,63 @@
+/-
+Copyright (c) 2022 Mac Malone. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Mac Malone
+-/
+prelude
+import Lean.Elab.Eval
+import Lean.Elab.ElabRules
+import Lake.Util.FilePath
+import Lake.DSL.Syntax
+
+/-!
+Syntax for elaboration time control flow.
+-/
+
+namespace Lake.DSL
+open Lean Meta Elab Command Term
+
+@[implemented_by Term.evalTerm]
+opaque evalTerm (α) (type : Expr) (value : Syntax) (safety := DefinitionSafety.safe) : TermElabM α
+
+def expandCmdDo : TSyntax ``cmdDo → Array Command
+| `(cmdDo|do $cmds*) => cmds
+| `(cmdDo|$cmd:command) => #[cmd]
+| _ => #[]
+
+@[builtin_command_elab metaIf]
+def elabMetaIf : CommandElab := fun stx => do
+  let `(meta if $c then $t $[else $e?]?) := stx
+    | throwErrorAt stx "ill-formed meta if command"
+  if (← withRef c <| runTermElabM fun _ => evalTerm Bool (toTypeExpr Bool) c .unsafe) then
+    let cmd := mkNullNode (expandCmdDo t)
+    withMacroExpansion (← getRef) cmd <| elabCommand cmd
+  else if let some e := e? then
+    let cmd := mkNullNode (expandCmdDo e)
+    withMacroExpansion (← getRef) cmd <| elabCommand cmd
+
+@[implemented_by Meta.evalExpr]
+opaque evalExpr (α) (expectedType : Expr) (value : Expr) (safety := DefinitionSafety.safe) : MetaM α
+
+def toExprIO [ToExpr α] (x : IO α) : IO Expr :=
+  toExpr <$> x
+
+@[builtin_term_elab runIO]
+def elabRunIO : TermElab := fun stx expectedType? =>
+  match stx with
+  | `(run_io%$tk $t) => withRef t do
+    let expectedType := mkApp (mkConst ``IO) <|
+      expectedType?.getD <| ← mkFreshExprMVar <| mkSort <| .succ .zero
+    let v ← elabTermEnsuringType (← `(do $t)) expectedType
+    synthesizeSyntheticMVarsNoPostponing
+    let v ← instantiateMVars v
+    if (← logUnassignedUsingErrorInfos (← getMVars v)) then
+      throwAbortTerm
+    let v ← mkAppM ``toExprIO #[v]
+    let io ← evalExpr (IO Expr) (mkApp (mkConst ``IO) (mkConst ``Expr)) v
+    let (out, x) ← IO.FS.withIsolatedStreams io.toBaseIO
+    unless out.isEmpty do
+      logInfoAt tk out
+    match x with
+    | .ok x => return x
+    | .error e => throwErrorAt tk e.toString
+  | _ => Elab.throwUnsupportedSyntax

backend/core/leanprover--lean4---v4.22.0/src/lean/lake/Lake/DSL/Package.lean

@@ -0,0 +1,54 @@
+/-
+Copyright (c) 2021 Mac Malone. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Mac Malone
+-/
+prelude
+import Lake.Config.Package
+import Lake.DSL.Attributes
+import Lake.DSL.DeclUtil
+import Lake.DSL.Syntax
+
+open Lean Parser Elab Command
+
+namespace Lake.DSL
+
+/-! # Package Declarations
+DSL definitions for packages and hooks.
+-/
+
+@[builtin_command_elab packageCommand]
+def elabPackageCommand : CommandElab := fun stx => do
+  let `(packageCommand|$(doc?)? $(attrs?)? package%$kw $[$nameStx?]? $cfg) := stx
+    | throwErrorAt stx "ill-formed package declaration"
+  withRef kw do
+  let configId : Ident ← `(pkgConfig)
+  let id ← mkConfigDeclIdent nameStx?
+  let name := Name.quoteFrom id id.getId
+  let ty := Syntax.mkCApp ``PackageConfig #[name]
+  elabConfig ``PackageConfig configId ty cfg
+  let attr ← `(Term.attrInstance| «package»)
+  let attrs := #[attr] ++ expandAttrs attrs?
+  let id := mkIdentFrom id packageDeclName
+  let decl ← `({name := $name, config := $configId})
+  let cmd ← `($[$doc?]? @[$attrs,*] abbrev $id : PackageDecl := $decl)
+  withMacroExpansion stx cmd <| elabCommand cmd
+
+abbrev PackageCommand := TSyntax ``packageCommand
+
+instance : Coe PackageCommand Command where
+  coe x := ⟨x.raw⟩
+
+@[builtin_macro postUpdateDecl]
+def expandPostUpdateDecl : Macro := fun stx => do
+  match stx with
+  | `($[$doc?]? $[$attrs?]? post_update%$kw $[$pkg?]? do $seq $[$wds?:whereDecls]?) =>
+    `($[$doc?]? $[$attrs?]? post_update%$kw $[$pkg?]? := do $seq $[$wds?:whereDecls]?)
+  | `($[$doc?]? $[$attrs?]? post_update%$kw $[$pkg?]? := $defn $[$wds?:whereDecls]?) => withRef kw do
+    let pkg ← expandOptSimpleBinder pkg?
+    let pkgName := mkIdentFrom pkg `_package.name
+    let attr ← `(Term.attrInstance| «post_update»)
+    let attrs := #[attr] ++ expandAttrs attrs?
+    `($[$doc?]? @[$attrs,*] def postUpdateHook : PostUpdateHookDecl :=
+      {pkg := $pkgName, fn := fun $pkg => $defn} $[$wds?:whereDecls]?)
+  | stx => Macro.throwErrorAt stx "ill-formed post_update declaration"

backend/core/leanprover--lean4---v4.22.0/src/lean/lake/Lake/DSL/Require.lean

@@ -0,0 +1,70 @@
+/-
+Copyright (c) 2021 Mac Malone. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Mac Malone
+-/
+prelude
+import Lean.Parser.Command
+import Lake.Config.Dependency
+import Lake.DSL.Extensions
+import Lake.DSL.DeclUtil
+import Lake.DSL.Syntax
+
+open Lean Parser Command
+
+namespace Lake.DSL
+
+/-! # The `require` syntax
+
+This module contains the expansion of the `require` DSL syntax used to specify package dependencies.
+-/
+
+@[inline] private def quoteOptTerm [Monad m] [MonadQuotation m] (term? : Option Term) : m Term :=
+  if let some term := term? then withRef term ``(some $term) else ``(none)
+
+def expandDepSpec (stx : TSyntax ``depSpec) (doc? : Option DocComment) : MacroM Command := do
+  let `(depSpec| $fullNameStx $[@ $ver?]? $[from $src?]? $[with $opts?]?) := stx
+    | Macro.throwErrorAt stx "ill-formed require syntax"
+  let src? ← src?.mapM fun src =>
+    match src with
+    | `(fromSource|git%$tk $url $[@ $rev?]? $[/ $subDir?]?) => withRef tk do
+      let rev ← quoteOptTerm rev?
+      let subDir ← quoteOptTerm subDir?
+      ``(DependencySrc.git $url $rev $subDir)
+    | `(fromSource|$path:term) => withRef src do
+      ``(DependencySrc.path $path)
+    | _ => Macro.throwErrorAt src "ill-formed from syntax"
+  let `(depName|$[$scope? /]? $nameStx) := fullNameStx
+    | Macro.throwErrorAt fullNameStx "ill-formed name syntax"
+  let scope :=
+    match scope? with
+    | some scope => scope
+    | none => Syntax.mkStrLit "" (.fromRef fullNameStx)
+  let ver ←
+    if let some ver := ver? then withRef ver do
+      match ver with
+      | `(verSpec|git $ver) => ``(some ("git#" ++ $ver))
+      | `(verSpec|$ver:term) => ``(some $ver)
+      | _ => Macro.throwErrorAt ver "ill-formed version syntax"
+    else
+      ``(none)
+  let name := expandIdentOrStrAsIdent nameStx
+  `($[$doc?:docComment]? @[package_dep] def $name : $(mkCIdent ``Dependency) := {
+    name :=  $(quote name.getId),
+    scope := $scope,
+    version? := $ver,
+    src? := $(← quoteOptTerm src?),
+    opts := $(opts?.getD <| ← `({})),
+  })
+
+
+@[builtin_macro requireDecl]
+def expandRequireDecl : Macro := fun stx => do
+  let `(requireDecl|$(doc?)? require%$kw $spec) := stx
+    | Macro.throwErrorAt stx "ill-formed require declaration"
+  withRef kw do expandDepSpec spec doc?
+
+@[inherit_doc requireDecl] abbrev RequireDecl := TSyntax ``requireDecl
+
+instance : Coe RequireDecl Command where
+  coe x := ⟨x.raw⟩

backend/core/leanprover--lean4---v4.22.0/src/lean/lake/Lake/DSL/Script.lean

@@ -0,0 +1,27 @@
+/-
+Copyright (c) 2021 Mac Malone. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Mac Malone
+-/
+prelude
+import Lake.Config.Package
+import Lake.DSL.Attributes
+import Lake.DSL.Syntax
+
+/-! # Script Declarations
+DSL definitions to define a Lake script for a package.
+-/
+
+namespace Lake.DSL
+open Lean Parser Command
+
+@[builtin_macro scriptDecl]
+def expandScriptDecl : Macro
+| `($[$doc?]? $[$attrs?]? script%$kw $name $[$args?]? do $seq $[$wds?:whereDecls]?) => do
+  `($[$doc?]? $[$attrs?]? script%$kw $name $[$args?]? := do $seq $[$wds?:whereDecls]?)
+| `($[$doc?]? $[$attrs?]? script%$kw $name $[$args?]? := $defn $[$wds?:whereDecls]?) => withRef kw do
+  let id := expandIdentOrStrAsIdent name
+  let args ← expandOptSimpleBinder args?
+  let attrs := #[← `(Term.attrInstance| «script»)] ++ expandAttrs attrs?
+  `($[$doc?]? @[$attrs,*] def $id : ScriptFn := fun $args => $defn $[$wds?:whereDecls]?)
+| stx => Macro.throwErrorAt stx "ill-formed script declaration"

backend/core/leanprover--lean4---v4.22.0/src/lean/lake/Lake/DSL/Syntax.lean

@@ -0,0 +1,419 @@
+/-
+Copyright (c) 2021 Mac Malone. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Mac Malone
+-/
+prelude
+import Lake.DSL.DeclUtil
+import Lean.Parser.Term
+
+open Lean Parser Elab Command
+
+open System (FilePath)
+
+/-!
+This module defines the syntax of the Lake DSL. The syntax is defined separately from the elaborator
+and/or macro definitions to allow clients to import it without crashing Lean. In particular, this
+allows the reference manual to document the DSL syntax.
+-/
+
+namespace Lake.DSL
+
+/--
+A macro that expands to the path of package's directory
+during the Lakefile's elaboration.
+-/
+scoped syntax (name := dirConst) "__dir__" : term
+
+/--
+A macro that expands to the specified configuration option (or `none`,
+if the option has not been set) during the Lakefile's elaboration.
+
+Configuration arguments are set either via the Lake CLI (by the `-K` option)
+or via the `with` clause in a `require` statement.
+-/
+scoped syntax (name := getConfig) "get_config? " ident :term
+
+/-!
+# Package Declarations
+DSL syntax definitions for packages and hooks.
+-/
+
+/--
+Defines the configuration of a Lake package.  Has many forms:
+
+```lean
+package «pkg-name»
+package «pkg-name» { /- config opts -/ }
+package «pkg-name» where /- config opts -/
+```
+
+There can only be one `package` declaration per Lake configuration file.
+The defined package configuration will be available for reference as `_package`.
+-/
+scoped syntax (name := packageCommand)
+(docComment)? (Term.attributes)? "package " (identOrStr)? optConfig : command
+
+/--
+Declare a post-`lake update` hook for the package.
+Runs the monadic action is after a successful `lake update` execution
+in this package or one of its downstream dependents.
+
+**Example**
+
+This feature enables Mathlib to synchronize the Lean toolchain and run
+`cache get` after a `lake update`:
+
+```
+lean_exe cache
+post_update pkg do
+  let wsToolchainFile := (← getRootPackage).dir / "lean-toolchain"
+  let mathlibToolchain ← IO.FS.readFile <| pkg.dir / "lean-toolchain"
+  IO.FS.writeFile wsToolchainFile mathlibToolchain
+  let exeFile ← runBuild cache.fetch
+  let exitCode ← env exeFile.toString #["get"]
+  if exitCode ≠ 0 then
+    error s!"{pkg.name}: failed to fetch cache"
+```
+-/
+scoped syntax (name := postUpdateDecl)
+optional(docComment) optional(Term.attributes)
+"post_update " (ppSpace simpleBinder)? (declValSimple <|> declValDo)
+: command
+
+
+/-! # The `require` syntax
+
+This is the `require` DSL syntax used to specify package dependencies.
+-/
+
+syntax fromPath :=
+  term
+
+syntax fromGit :=
+  &"git " term:max ("@" term:max)? ("/" term)?
+
+syntax fromSource :=
+  fromGit <|> fromPath
+
+/--
+Specifies a specific source from which to draw the package dependency.
+Dependencies that are downloaded from a remote source will be placed
+into the workspace's `packagesDir`.
+
+**Path Dependencies**
+
+```
+from <path>
+```
+
+Lake loads the package located a fixed `path` relative to the
+requiring package's directory.
+
+**Git Dependencies**
+
+```
+from git <url> [@ <rev>] [/ <subDir>]
+```
+
+Lake clones the Git repository available at the specified fixed Git `url`,
+and checks out the specified revision `rev`. The revision can be a commit hash,
+branch, or tag. If none is provided, Lake defaults to `master`. After checkout,
+Lake loads the package located in `subDir` (or the repository root if no
+subdirectory is specified).
+-/
+syntax fromClause :=
+  " from " fromSource
+
+/-
+A `NameMap String` of Lake options used to configure the dependency.
+This is equivalent to passing `-K` options to the dependency on the command line.
+-/
+syntax withClause :=
+  " with " term
+
+syntax verSpec :=
+  &"git "? term:max
+
+/--
+The version of the package to require.
+To specify a Git revision, use the syntax `@ git <rev>`.
+-/
+syntax verClause :=
+  " @ " verSpec
+
+syntax depName :=
+  atomic(str " / ")? identOrStr
+
+syntax depSpec :=
+  depName (verClause)? (fromClause)? (withClause)?
+
+/--
+Adds a new package dependency to the workspace. The general syntax is:
+
+```
+require ["<scope>" /] <pkg-name> [@ <version>]
+  [from <source>] [with <options>]
+```
+
+The `from` clause tells Lake where to locate the dependency.
+See the `fromClause` syntax documentation (e.g., hover over it) to see
+the different forms this clause can take.
+
+Without a `from` clause, Lake will lookup the package in the default
+registry (i.e., Reservoir) and use the information there to download the
+package at the requested `version`. The `scope` is used to disambiguate between
+packages in the registry with the same `pkg-name`. In Reservoir, this scope
+is the package owner (e.g., `leanprover` of `@leanprover/doc-gen4`).
+
+The `with` clause specifies a `NameMap String` of Lake options
+used to configure the dependency. This is equivalent to passing `-K`
+options to the dependency on the command line.
+-/
+scoped syntax (name := requireDecl)
+(docComment)? "require " depSpec : command
+
+
+/-!
+# DSL for Targets & Facets
+Syntax for declaring Lake targets and facets.
+-/
+
+syntax buildDeclSig :=
+  identOrStr (ppSpace simpleBinder)? Term.typeSpec declValSimple
+
+/-!
+## Facet Declarations
+-/
+
+/--
+Define a new module facet. Has one form:
+
+```lean
+module_facet «facet-name» (mod : Module) : α :=
+  /- build term of type `FetchM (Job α)` -/
+```
+
+The `mod` parameter (and its type specifier) is optional.
+-/
+scoped syntax (name := moduleFacetDecl)
+(docComment)? (Term.attributes)? "module_facet " buildDeclSig : command
+
+/--
+Define a new package facet. Has one form:
+
+```lean
+package_facet «facet-name» (pkg : Package) : α :=
+  /- build term of type `FetchM (Job α)` -/
+```
+
+The `pkg` parameter (and its type specifier) is optional.
+-/
+scoped syntax (name := packageFacetDecl)
+(docComment)? (Term.attributes)? "package_facet " buildDeclSig : command
+
+/--
+Define a new library facet. Has one form:
+
+```lean
+library_facet «facet-name» (lib : LeanLib) : α :=
+  /- build term of type `FetchM (Job α)` -/
+```
+
+The `lib` parameter (and its type specifier) is optional.
+-/
+scoped syntax (name := libraryFacetDecl)
+(docComment)? (Term.attributes)? "library_facet " buildDeclSig : command
+
+
+/-!
+## Custom Target Declaration
+-/
+
+/--
+Define a new custom target for the package. Has one form:
+
+```lean
+target «target-name» (pkg : NPackage _package.name) : α :=
+  /- build term of type `FetchM (Job α)` -/
+```
+
+The `pkg` parameter (and its type specifier) is optional.
+It is of type `NPackage _package.name` to provably demonstrate the package
+provided is the package in which the target is defined.
+-/
+scoped syntax (name := targetCommand)
+(docComment)? (Term.attributes)? "target " buildDeclSig : command
+
+
+/-!
+## Lean Library & Executable Target Declarations
+-/
+
+/--
+Define a new Lean library target for the package.
+Can optionally be provided with a configuration of type `LeanLibConfig`.
+Has many forms:
+
+```lean
+lean_lib «target-name»
+lean_lib «target-name» { /- config opts -/ }
+lean_lib «target-name» where /- config opts -/
+```
+-/
+scoped syntax (name := leanLibCommand)
+(docComment)? (Term.attributes)? "lean_lib " (identOrStr)? optConfig : command
+
+/--
+Define a new Lean binary executable target for the package.
+Can optionally be provided with a configuration of type `LeanExeConfig`.
+Has many forms:
+
+```lean
+lean_exe «target-name»
+lean_exe «target-name» { /- config opts -/ }
+lean_exe «target-name» where /- config opts -/
+```
+-/
+scoped syntax (name := leanExeCommand)
+(docComment)? (Term.attributes)? "lean_exe " (identOrStr)? optConfig : command
+
+/--
+Define a new input file target for the package.
+Can optionally be provided with a configuration of type `InputFileConfig`.
+-/
+scoped syntax (name := inputFileCommand)
+(docComment)? (Term.attributes)? "input_file " (identOrStr)? optConfig : command
+
+/--
+Define a new input directory target for the package.
+Can optionally be provided with a configuration of type `InputDirConfig`.
+-/
+scoped syntax (name := inputDirCommand)
+(docComment)? (Term.attributes)? "input_dir " (identOrStr)? optConfig : command
+
+/-!
+## External Library Target Declaration
+-/
+
+syntax externLibDeclSpec :=
+  identOrStr (ppSpace simpleBinder)? declValSimple
+
+/--
+Define a new external library target for the package. Has one form:
+
+```lean
+extern_lib «target-name» (pkg : NPackage _package.name) :=
+  /- build term of type `FetchM (Job FilePath)` -/
+```
+
+The `pkg` parameter (and its type specifier) is optional.
+It is of type `NPackage _package.name` to provably demonstrate the package
+provided is the package in which the target is defined.
+
+The term should build the external library's **static** library.
+-/
+scoped syntax (name := externLibCommand)
+(docComment)? (Term.attributes)? "extern_lib " externLibDeclSpec : command
+
+/-!
+# Script Declarations
+
+DSL definitions to define a Lake script for a package.
+-/
+
+syntax scriptDeclSpec :=
+  identOrStr (ppSpace simpleBinder)? (declValSimple <|> declValDo)
+
+/--
+Define a new Lake script for the package.
+
+**Example**
+
+```
+/-- Display a greeting -/
+script «script-name» (args) do
+  if h : 0 < args.length then
+    IO.println s!"Hello, {args[0]'h}!"
+  else
+    IO.println "Hello, world!"
+  return 0
+```
+-/
+scoped syntax (name := scriptDecl)
+(docComment)? optional(Term.attributes) "script " scriptDeclSpec : command
+
+end DSL
+
+/-!
+# Version Literals
+
+Defines the `v!"<ver>"` syntax for version literals.
+-/
+
+/-- A Lake version literal. -/
+scoped syntax:max (name := verLit) "v!" noWs interpolatedStr(term) : term
+
+namespace DSL
+
+/-!
+# DSL for Build Key
+
+Notation for specifying build keys in a package.
+-/
+
+syntax facetSuffix := atomic(":" noWs) ident
+syntax packageTargetLit := atomic("+" noWs)? ident
+
+/-- A module target key literal (with optional facet). -/
+scoped syntax:max "`+" noWs ident facetSuffix* : term
+
+/-- A package target key literal (with optional facet). -/
+scoped syntax:max "`@" (noWs ident)?
+  (atomic(noWs "/" noWs) packageTargetLit)? (noWs facetSuffix)* : term
+
+/-!
+# Elaboration-Time Control Flow
+
+Syntax for elaboration time control flow.
+-/
+
+/--
+The `do` command syntax groups multiple similarly indented commands together.
+The group can then be passed to another command that usually only accepts a
+single command (e.g., `meta if`).
+-/
+syntax cmdDo := ("do" many1Indent(command)) <|> command
+
+/--
+The `meta if` command has two forms:
+
+```lean
+meta if <c:term> then <a:command>
+meta if <c:term> then <a:command> else <b:command>
+```
+
+It expands to the command `a` if the term `c` evaluates to true
+(at elaboration time). Otherwise, it expands to command `b` (if an `else`
+clause is provided).
+
+One can use this command to specify, for example, external library targets
+only available on specific platforms:
+
+```lean
+meta if System.Platform.isWindows then
+extern_lib winOnlyLib := ...
+else meta if System.Platform.isOSX then
+extern_lib macOnlyLib := ...
+else
+extern_lib linuxOnlyLib := ...
+```
+-/
+scoped syntax (name := metaIf)
+"meta " "if " term " then " cmdDo (" else " cmdDo)? : command
+
+/--
+Executes a term of type `IO α` at elaboration-time
+and produces an expression corresponding to the result via `ToExpr α`.
+-/
+scoped syntax:lead (name := runIO) "run_io " doSeq : term

backend/core/leanprover--lean4---v4.22.0/src/lean/lake/Lake/DSL/Targets.lean

@@ -0,0 +1,257 @@
+/-
+Copyright (c) 2022 Mac Malone. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Mac Malone
+-/
+prelude
+import Lake.DSL.DeclUtil
+import Lake.DSL.Syntax
+import Lake.Config.FacetConfig
+import Lake.Config.TargetConfig
+import Lake.Build.Job
+
+
+/-! # DSL for Targets & Facets
+Macros for declaring Lake targets and facets.
+-/
+
+open System (FilePath)
+open Lean Parser Elab Command
+
+namespace Lake.DSL
+
+
+--------------------------------------------------------------------------------
+/-! ## Facet Declarations                                                      -/
+--------------------------------------------------------------------------------
+
+abbrev mkModuleFacetDecl
+  (α) (facet : Name)
+  [OptDataKind α] [FormatQuery α] [FamilyDef ModuleData facet α]
+  (f : Module → FetchM (Job α))
+: ModuleFacetDecl := .mk (Module.facetKind ++ facet) <| mkFacetJobConfig fun mod => do
+  withRegisterJob (mod.facet facet |>.key.toSimpleString)
+    (f mod)
+
+@[builtin_macro moduleFacetDecl]
+def expandModuleFacetDecl : Macro := fun stx => do
+  let `(moduleFacetDecl|$(doc?)? $(attrs?)? module_facet%$kw $sig) := stx
+    | Macro.throwErrorAt stx "ill-formed module facet declaration"
+  let `(buildDeclSig| $nameStx $[$mod?]? : $ty := $defn $[$wds?:whereDecls]?) := sig
+    | Macro.throwErrorAt sig "ill-formed module facet declaration"
+  withRef kw do
+  let attr ← `(Term.attrInstance| «module_facet»)
+  let attrs := #[attr] ++ expandAttrs attrs?
+  let id := expandIdentOrStrAsIdent nameStx
+  let facet := Name.quoteFrom id id.getId
+  let declId := mkIdentFrom id <| id.getId.modifyBase (.str · "_modFacet")
+  let mod ← expandOptSimpleBinder mod?
+  `(module_data $id : $ty
+    $[$doc?:docComment]? @[$attrs,*] abbrev $declId :=
+      Lake.DSL.mkModuleFacetDecl $ty $facet (fun $mod => $defn)
+    $[$wds?:whereDecls]?)
+
+abbrev mkPackageFacetDecl
+  (α) (facet : Name)
+  [OptDataKind α] [FormatQuery α] [FamilyDef PackageData facet α]
+  (f : Package → FetchM (Job α))
+: PackageFacetDecl := .mk (Package.facetKind ++ facet) <| mkFacetJobConfig fun pkg => do
+  withRegisterJob (pkg.facet facet |>.key.toSimpleString)
+    (f pkg)
+
+@[builtin_macro packageFacetDecl]
+def expandPackageFacetDecl : Macro := fun stx => do
+  let `(packageFacetDecl|$(doc?)? $(attrs?)? package_facet%$kw $sig) := stx
+    | Macro.throwErrorAt stx "ill-formed package facet declaration"
+  let `(buildDeclSig| $nameStx $[$pkg?]? : $ty := $defn $[$wds?:whereDecls]?) := sig
+    | Macro.throwErrorAt sig "ill-formed package facet signature"
+  withRef kw do
+  let attr ← `(Term.attrInstance| «package_facet»)
+  let attrs := #[attr] ++ expandAttrs attrs?
+  let id := expandIdentOrStrAsIdent nameStx
+  let facet := Name.quoteFrom id id.getId
+  let declId := mkIdentFrom id <| id.getId.modifyBase (.str · "_pkgFacet")
+  let pkg ← expandOptSimpleBinder pkg?
+  `(package_data $id : $ty
+    $[$doc?]? @[$attrs,*] abbrev $declId :=
+      Lake.DSL.mkPackageFacetDecl $ty $facet (fun $pkg => $defn)
+    $[$wds?:whereDecls]?)
+
+abbrev mkLibraryFacetDecl
+  (α) (facet : Name)
+  [OptDataKind α] [FormatQuery α] [FamilyDef LibraryData facet α]
+  (f : LeanLib → FetchM (Job α))
+: LibraryFacetDecl := .mk (LeanLib.facetKind ++ facet) <| mkFacetJobConfig fun lib => do
+  withRegisterJob (lib.facet facet |>.key.toSimpleString)
+    (f lib)
+
+@[builtin_macro libraryFacetDecl]
+def expandLibraryFacetDecl : Macro := fun stx => do
+  let `(libraryFacetDecl|$(doc?)? $(attrs?)? library_facet%$kw $sig) := stx
+    | Macro.throwErrorAt stx "ill-formed library facet declaration"
+  let `(buildDeclSig| $nameStx  $[$lib?]? : $ty := $defn $[$wds?:whereDecls]?) := sig
+    | Macro.throwErrorAt sig "ill-formed library facet signature"
+  withRef kw do
+  let attr ← `(Term.attrInstance| «library_facet»)
+  let attrs := #[attr] ++ expandAttrs attrs?
+  let id := expandIdentOrStrAsIdent nameStx
+  let facet := Name.quoteFrom id id.getId
+  let declId := mkIdentFrom id <| id.getId.modifyBase (.str · "_libFacet")
+  let lib ← expandOptSimpleBinder lib?
+  `(library_data $id : $ty
+    $[$doc?]? @[$attrs,*] abbrev $declId : LibraryFacetDecl :=
+      Lake.DSL.mkLibraryFacetDecl $ty $facet (fun $lib => $defn)
+    $[$wds?:whereDecls]?)
+
+
+--------------------------------------------------------------------------------
+/-! ## Custom Target Declaration                                              -/
+--------------------------------------------------------------------------------
+
+abbrev mkTargetDecl
+  (α) (pkgName «target» : Name)
+  [OptDataKind α] [FormatQuery α] [FamilyDef (CustomData pkgName) «target» α]
+  (f : NPackage pkgName → FetchM (Job α))
+: TargetDecl :=
+  let cfg := mkTargetJobConfig fun pkg => do
+    withRegisterJob (pkg.target «target» |>.key.toSimpleString) do
+      f pkg
+  .mk (.mk pkgName «target» .anonymous (.mk cfg) (by simp [Name.isAnonymous])) rfl
+
+@[builtin_macro targetCommand]
+def expandTargetCommand : Macro := fun stx => do
+  let `(targetCommand|$(doc?)? $(attrs?)? target%$kw $sig) := stx
+    | Macro.throwErrorAt stx "ill-formed target declaration"
+  let `(buildDeclSig|$id:ident $[$pkg?]? : $ty := $defn $[$wds?:whereDecls]?) := sig
+    | Macro.throwErrorAt sig "ill-formed target signature"
+  withRef kw do
+  let attr ← `(Term.attrInstance| «target»)
+  let attrs := #[attr] ++ expandAttrs attrs?
+  let name := Name.quoteFrom id id.getId
+  let pkgName := mkIdentFrom id (packageDeclName.str "name")
+  let pkg ← expandOptSimpleBinder pkg?
+  `(family_def $id : CustomOut ($pkgName, $name) := $ty
+    $[$doc?]? abbrev $id :=
+      Lake.DSL.mkTargetDecl $ty $pkgName $name (fun $pkg => $defn)
+    $[$wds?:whereDecls]?
+    @[$attrs,*] def configDecl : ConfigDecl := $(id).toConfigDecl)
+
+--------------------------------------------------------------------------------
+/-! ## Lean Library & Executable Target Declarations -/
+--------------------------------------------------------------------------------
+
+abbrev mkConfigDecl
+  (pkg name kind : Name)
+  (config : ConfigType kind pkg name)
+  [FamilyDef (CustomData pkg) name (ConfigTarget kind)]
+  [FamilyDef DataType kind (ConfigTarget kind)]
+: KConfigDecl kind :=
+  {pkg, name, kind, config, wf_data := fun _ => by simp, kind_eq := rfl}
+
+def mkConfigDeclDef
+  (tyName attr kind : Name)
+  [ConfigInfo tyName] [delTyName : TypeName (KConfigDecl kind)]
+  (doc? : Option DocComment) (attrs? : Option Attributes)
+  (nameStx? : Option IdentOrStr) (cfg : OptConfig)
+: CommandElabM Command := do
+  let configId : Ident ← `(config)
+  let id ← mkConfigDeclIdent nameStx?
+  let name := Name.quoteFrom id id.getId
+  let ty := Syntax.mkCApp tyName #[name]
+  elabConfig tyName configId ty cfg
+  let attrId ← mkIdentFromRef attr
+  let targetAttr ← `(Term.attrInstance| «target»)
+  let kindAttr ← `(Term.attrInstance| $attrId:ident)
+  let attrs := #[targetAttr, kindAttr] ++ expandAttrs attrs?
+  let pkg ← mkIdentFromRef (packageDeclName.str "name")
+  let declTy ← mkIdentFromRef delTyName.typeName
+  let kind := Name.quoteFrom (← getRef) kind
+  `(family_def $id : CustomOut ($pkg, $name) := ConfigTarget $kind
+    $[$doc?]? abbrev $id : $declTy :=
+      Lake.DSL.mkConfigDecl $pkg $name $kind $configId
+    @[$attrs,*] def configDecl : ConfigDecl := $(id).toConfigDecl
+  )
+
+@[builtin_command_elab leanLibCommand]
+def elabLeanLibCommand : CommandElab := fun stx => do
+  let `(leanLibCommand|$(doc?)? $(attrs?)? lean_lib%$kw $(nameStx?)? $cfg) := stx
+    | throwErrorAt stx "ill-formed lean_lib declaration"
+  withRef kw do
+  let cmd ← mkConfigDeclDef ``LeanLibConfig LeanLib.keyword LeanLib.configKind doc? attrs? nameStx? cfg
+  withMacroExpansion stx cmd <| elabCommand cmd
+
+@[inherit_doc leanLibCommand] abbrev LeanLibCommand := TSyntax ``leanLibCommand
+
+instance : Coe LeanLibCommand Command where
+  coe x := ⟨x.raw⟩
+
+@[builtin_command_elab leanExeCommand]
+def elabLeanExeCommand : CommandElab := fun stx => do
+  let `(leanExeCommand|$(doc?)? $(attrs?)? lean_exe%$kw $(nameStx?)? $cfg) := stx
+    | throwErrorAt stx "ill-formed lean_exe declaration"
+  withRef kw do
+  let cmd ← mkConfigDeclDef ``LeanExeConfig LeanExe.keyword LeanExe.configKind doc? attrs? nameStx? cfg
+  withMacroExpansion stx cmd <| elabCommand cmd
+
+@[inherit_doc leanExeCommand] abbrev LeanExeCommand := TSyntax ``leanExeCommand
+
+instance : Coe LeanExeCommand Command where
+  coe x := ⟨x.raw⟩
+
+@[builtin_command_elab inputFileCommand]
+def elabInputfileCommand : CommandElab := fun stx => do
+  let `(inputFileCommand|$(doc?)? $(attrs?)? input_file%$kw $(nameStx?)? $cfg) := stx
+    | throwErrorAt stx "ill-formed input_file declaration"
+  withRef kw do
+  let cmd ← mkConfigDeclDef ``InputFileConfig InputFile.keyword InputFile.configKind doc? attrs? nameStx? cfg
+  withMacroExpansion stx cmd <| elabCommand cmd
+
+@[inherit_doc inputFileCommand] abbrev InputFileCommand := TSyntax ``inputFileCommand
+
+instance : Coe InputFileCommand Command where
+  coe x := ⟨x.raw⟩
+
+@[builtin_command_elab inputDirCommand]
+def elabInputDirCommand : CommandElab := fun stx => do
+  let `(inputDirCommand|$(doc?)? $(attrs?)? input_dir%$kw $(nameStx?)? $cfg) := stx
+    | throwErrorAt stx "ill-formed input_dir declaration"
+  withRef kw do
+  let cmd ← mkConfigDeclDef ``InputDirConfig InputDir.keyword InputDir.configKind doc? attrs? nameStx? cfg
+  withMacroExpansion stx cmd <| elabCommand cmd
+
+@[inherit_doc inputDirCommand] abbrev InputDirCommand := TSyntax ``inputDirCommand
+
+instance : Coe InputDirCommand Command where
+  coe x := ⟨x.raw⟩
+
+--------------------------------------------------------------------------------
+/-! ## External Library Target Declaration                                    -/
+--------------------------------------------------------------------------------
+
+abbrev mkExternLibDecl
+  (pkgName name : Name)
+  [FamilyDef (CustomData pkgName) (.str name "static") FilePath]
+  [FamilyDef (CustomData pkgName) name (ConfigTarget ExternLib.configKind)]
+: ExternLibDecl :=
+  mkConfigDecl pkgName name ExternLib.configKind {getPath := cast (by simp)}
+
+@[builtin_macro externLibCommand]
+def expandExternLibCommand : Macro := fun stx => do
+  let `(externLibCommand|$(doc?)? $(attrs?)? extern_lib%$kw $spec) := stx
+    | Macro.throwErrorAt stx "ill-formed external library declaration"
+  let `(externLibDeclSpec| $nameStx $[$pkg?]? := $defn $[$wds?:whereDecls]?) := spec
+    | Macro.throwErrorAt spec "ill-formed external library signature"
+  withRef kw do
+  let attr1 ← `(Term.attrInstance| «target»)
+  let attr2 ← `(Term.attrInstance| «extern_lib»)
+  let attrs := #[attr1, attr2] ++ expandAttrs attrs?
+  let id := expandIdentOrStrAsIdent nameStx
+  let pkgName := mkIdentFrom kw (packageDeclName.str "name")
+  let targetId := mkIdentFrom id <| id.getId.modifyBase (· ++ `static)
+  let name := Name.quoteFrom id id.getId
+  let kind := Name.quoteFrom kw ExternLib.configKind
+  `(target $targetId:ident $[$pkg?]? : FilePath := $defn $[$wds?:whereDecls]?
+    family_def $id : CustomOut ($pkgName, $name) := ConfigTarget $kind
+    $[$doc?:docComment]? def $id : ExternLibDecl :=
+      Lake.DSL.mkExternLibDecl $pkgName $name
+    @[$attrs,*] def configDecl : ConfigDecl := $(id).toConfigDecl)

backend/core/leanprover--lean4---v4.22.0/src/lean/lake/Lake/DSL/VerLit.lean

@@ -0,0 +1,47 @@
+/-
+Copyright (c) 2024 Mac Malone. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Mac Malone
+-/
+prelude
+import Lean.Elab.Eval
+import Lake.Util.Version
+import Lake.DSL.Syntax
+
+open Lean Elab Term Meta
+
+/-! # Version Literals
+
+Defines the `v!"<ver>"` syntax for version literals.
+The elaborator attempts to synthesize an instance of `DecodeVersion` for the
+expected type and then applies it to the string literal.
+-/
+
+namespace Lake
+
+instance : ToExpr SemVerCore where
+  toExpr ver := mkAppN (mkConst ``SemVerCore.mk)
+    #[toExpr ver.major, toExpr ver.minor, toExpr ver.patch]
+  toTypeExpr := mkConst ``SemVerCore
+
+instance : ToExpr StdVer where
+  toExpr ver := mkAppN (mkConst ``StdVer.mk)
+    #[toExpr ver.toSemVerCore, toExpr ver.specialDescr]
+  toTypeExpr := mkConst ``StdVer
+
+private def toResultExpr [ToExpr α] (x : Except String α) : Except String Expr :=
+  Functor.map toExpr x
+
+@[builtin_term_elab verLit]
+def elabVerLit : TermElab := fun stx expectedType? => do
+  let `(v!$v) := stx | throwUnsupportedSyntax
+  tryPostponeIfNoneOrMVar expectedType?
+  let some expectedType := expectedType?
+    | throwError "expected type is not known"
+  let ofVerT? ← mkAppM ``Except #[mkConst ``String, expectedType]
+  let ofVerE ← elabTermEnsuringType (← ``(decodeVersion s!$v)) ofVerT?
+  let resT ← mkAppM ``Except #[mkConst ``String, mkConst ``Expr]
+  let resE ← mkAppM ``toResultExpr #[ofVerE]
+  match (← unsafe evalExpr (Except String Expr) resT resE) with
+  | .ok ver => return ver
+  | .error e => throwError e

backend/core/leanprover--lean4---v4.22.0/src/lean/lake/Lake/Load/Config.lean

@@ -0,0 +1,58 @@
+/-
+Copyright (c) 2022 Mac Malone. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Mac Malone
+-/
+prelude
+import Lean.Data.Name
+import Lean.Data.Options
+import Lake.Config.Env
+import Lake.Load.Manifest
+import Lake.Util.FilePath
+
+namespace Lake
+open System Lean
+
+/-- Context for loading a Lake configuration. -/
+structure LoadConfig where
+  /-- The Lake environment of the load process. -/
+  lakeEnv : Lake.Env
+  /--
+  The CLI arguments Lake was run with.
+  Used to perform a restart of Lake on a toolchain update.
+  A value of `none` means that Lake is not restartable via the CLI.
+  -/
+  lakeArgs? : Option (Array String) := none
+  /-- The absolute path to the root directory of the Lake workspace. -/
+  wsDir : FilePath
+  /-- The loaded package's directory (relative to the workspace directory). -/
+  relPkgDir : FilePath := "."
+  /-- The absolute path to the loaded package's directory. -/
+  pkgDir : FilePath := wsDir / relPkgDir
+  /-- The package's Lake configuration file (relative to its directory). -/
+  relConfigFile : FilePath := defaultConfigFile
+    /-- The full path to the loaded package's Lake configuration file. -/
+  configFile : FilePath := pkgDir / relConfigFile
+  /-- Additional package overrides for this workspace load. -/
+  packageOverrides : Array PackageEntry := #[]
+  /-- A set of key-value Lake configuration options (i.e., `-K` settings). -/
+  lakeOpts : NameMap String := {}
+  /-- The Lean options with which to elaborate the configuration file. -/
+  leanOpts : Options := {}
+  /-- Whether Lake should re-elaborate configuration files instead of using cached OLeans. -/
+  reconfigure : Bool := false
+  /-- Whether to update dependencies when loading the workspace. -/
+  updateDeps : Bool := false
+  /--
+  Whether to update the workspace's `lean-toolchain` when dependencies are updated.
+  If `true` and a toolchain update occurs, Lake will need to be restarted.
+  -/
+  updateToolchain : Bool := true
+  /-- The package's scope (e.g., in Reservoir). -/
+  scope : String := ""
+  /-- The URL to this package's Git remote (if any). -/
+  remoteUrl : String := ""
+
+/-- The package's Lake directory (for Lake temporary files). -/
+@[inline] def LoadConfig.lakeDir (cfg : LoadConfig) : FilePath :=
+  cfg.pkgDir / defaultLakeDir

backend/core/leanprover--lean4---v4.22.0/src/lean/lake/Lake/Load/Lean.lean

@@ -0,0 +1,37 @@
+/-
+Copyright (c) 2024 Mac Malone. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Mac Malone
+-/
+prelude
+import Lake.Load.Lean.Elab
+import Lake.Load.Lean.Eval
+
+/-! # Lean Loader
+
+This module contains the main definitions to load a package from a
+Lake configuration file written in Lake's Lean DSL.
+-/
+
+open Lean
+
+namespace Lake
+
+/--
+Elaborate a Lean configuration file into a `Package`.
+The resulting package does not yet include any dependencies.
+-/
+def loadLeanConfig (cfg : LoadConfig)
+: LogIO (Package × Environment) := do
+  let configEnv ← importConfigFile cfg
+  let {name, config} ← IO.ofExcept <| PackageDecl.loadFromEnv configEnv cfg.leanOpts
+  let pkg : Package := {
+    name, config
+    dir := cfg.pkgDir
+    relDir := cfg.relPkgDir
+    configFile := cfg.configFile
+    relConfigFile := cfg.relConfigFile
+    scope := cfg.scope
+    remoteUrl := cfg.remoteUrl
+  }
+  return (← pkg.loadFromEnv configEnv cfg.leanOpts, configEnv)

backend/core/leanprover--lean4---v4.22.0/src/lean/lake/Lake/Load/Lean/Elab.lean

@@ -0,0 +1,264 @@
+/-
+Copyright (c) 2021 Mac Malone. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Mac Malone
+-/
+prelude
+import Lean.Elab.Frontend
+import Lake.DSL.Extensions
+import Lake.DSL.Attributes
+import Lake.Load.Config
+import Lake.Build.Trace
+import Lake.Util.Log
+
+/-! # Lean Configuration Elaborator
+
+This module contains the definitions to elaborate a Lake configuration file.
+-/
+
+
+open System Lean
+
+namespace Lake
+
+deriving instance BEq, Hashable for Import
+
+/- Cache for the imported header environment of Lake configuration files. -/
+builtin_initialize importEnvCache : IO.Ref (Std.HashMap (Array Import) Environment) ← IO.mkRef {}
+
+/-- Like `importModules`, but fetch the resulting import state from the cache if possible. -/
+def importModulesUsingCache (imports : Array Import) (opts : Options) (trustLevel : UInt32) : IO Environment := do
+  if let some env := (← importEnvCache.get)[imports]? then
+    return env
+  let env ← importModules (loadExts := true) imports opts trustLevel
+  importEnvCache.modify (·.insert imports env)
+  return env
+
+/-- Like `Lean.Elab.processHeader`, but using `importEnvCache`. -/
+def processHeader (header : TSyntax ``Parser.Module.header) (opts : Options)
+(inputCtx : Parser.InputContext) : StateT MessageLog IO Environment := do
+  try
+    let imports := Elab.headerToImports header
+    importModulesUsingCache imports opts 1024
+  catch e =>
+    let pos := inputCtx.fileMap.toPosition <| header.raw.getPos?.getD 0
+    modify (·.add { fileName := inputCtx.fileName, data := toString e, pos })
+    mkEmptyEnvironment
+
+/-- Main module `Name` of a Lake configuration file. -/
+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 / defaultLeanConfigFile) : LogIO Environment := do
+
+  -- Read file and initialize environment
+  let input ← IO.FS.readFile configFile
+  let inputCtx := Parser.mkInputContext input configFile.toString
+  let (header, parserState, messages) ← Parser.parseHeader inputCtx
+  let (env, messages) ← processHeader header leanOpts inputCtx messages
+  let env := env.setMainModule configModuleName
+
+  -- Configure extensions
+  let env := dirExt.setState env pkgDir
+  let env := optsExt.setState env lakeOpts
+
+  -- Elaborate File
+  let commandState := Elab.Command.mkState env messages leanOpts
+  let s ← Elab.IO.processCommands inputCtx parserState commandState
+
+  -- Log messages
+  s.commandState.messages.forM (logMessage ·)
+
+  -- Check result
+  if s.commandState.messages.hasErrors then
+    error s!"{configFile}: package configuration has errors"
+  else
+    return s.commandState.env
+
+/--
+`Lean.Kernel.Environment.add` is now private, this is an exported helper wrapping it for
+`Lean.Environment`.
+-/
+@[extern "lake_environment_add"]
+private opaque addToEnv (env : Environment) (_ : ConstantInfo) : Environment
+
+/--
+Import a configuration `.olean` (e.g., `lakefile.olean`).
+Auxiliary definition for `importConfigFile`.
+-/
+def importConfigFileCore (olean : FilePath) (leanOpts : Options) : IO Environment := do
+  /-
+  We could import the olean together with its imports using one
+  `importModules` call, but that would mean we pay for a full
+  `finalizeImports` each time, which is linear in the number of imported
+  constants and extension entries (in fact, it is paid two more times: when
+  marking the `Environment` object as multi-threaded, and when releasing
+  it). As most lakefiles use the same set of imports, we instead construct
+  an `Environment` for it only once, and then apply the lakefile contents
+  on top of it like the elaborator would. Thus the non-shared part of the
+  `Environment` is very small.
+  -/
+  let (mod, _) ← readModuleData olean
+  let env ← importModulesUsingCache mod.imports leanOpts 1024
+  -- Apply constants (does not go through the kernel, so order is irrelevant)
+  let env := mod.constants.foldl addToEnv env
+  /-
+  Below, we pass module environment extension entries to
+  `PersistentEnvExtension.addEntryFn` - but for an extension of
+  non-erased type `PersistentEnvExtension α β σ`, the former are of type
+  `α` while `addEntryFn` expects `β`s (the type-erased
+  `persistentEnvExtensionsRef` ought to be `unsafe` to prevent this from
+  simply compiling but it isn't right now). Fortunately, all extensions
+  relevant for workspace loading, which we filter for here, have `α = β`;
+  entries for any other extensions can safely be ignored.
+  -/
+  let extDescrs ← persistentEnvExtensionsRef.get
+  let extNameIdx ← mkExtNameMap 0
+  let env := mod.entries.foldl (init := env) fun env (extName, ents) =>
+    if lakeExts.contains extName then
+      match extNameIdx[extName]? with
+      | some entryIdx => ents.foldl extDescrs[entryIdx]!.addEntry env
+      | none => env
+    else
+      env
+  return env
+where
+  lakeExts :=
+    NameSet.empty
+    -- Lake Persistent Extensions
+    |>.insert ``packageAttr
+    |>.insert ``packageDepAttr
+    |>.insert ``postUpdateAttr
+    |>.insert ``scriptAttr
+    |>.insert ``defaultScriptAttr
+    |>.insert ``leanLibAttr
+    |>.insert ``leanExeAttr
+    |>.insert ``externLibAttr
+    |>.insert ``targetAttr
+    |>.insert ``defaultTargetAttr
+    |>.insert ``testDriverAttr
+    |>.insert ``lintDriverAttr
+    |>.insert ``moduleFacetAttr
+    |>.insert ``packageFacetAttr
+    |>.insert ``libraryFacetAttr
+    -- Docstring Extension (e.g., for scripts)
+    |>.insert ``docStringExt
+    -- IR Extension (for constant evaluation)
+    |>.insert ``IR.declMapExt
+
+structure ConfigTrace where
+  platform : String
+  leanHash : String
+  configHash : Hash
+  options : NameMap String
+  deriving ToJson, FromJson
+
+/--
+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 (cfg : LoadConfig) : LogIO Environment := do
+  let some configName := FilePath.mk <$> cfg.configFile.fileName
+    | error "invalid configuration file name"
+  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
+  (i.e., one process writes a new configuration while another reads an old one
+  and vice versa), Lake performs file locking to ensure exclusive access.
+
+  To check if the trace is up-to-date, Lake opens a read-only handle on the
+  trace file and acquires a shared lock on it. The lock is held while the
+  trace is read and compared to the expected value. If it matches, the olean is
+  imported and the (shared) lock is then released.
+
+  If the trace is out-of-date, Lake upgrades the trace to read-write handle
+  with an exclusive lock. Lake does this by first acquiring a exclusive lock to
+  configuration's lock file (i.e. `olean.lock`). While holding this lock, Lake
+  releases the shared lock on the trace, re-opens the trace with a read-write
+  handle, and acquires an exclusive lock on the trace. It then releases its
+  lock on the lock file. writes the new lock data.
+  -/
+  let acquireTrace h : IO IO.FS.Handle := id do
+    let hLock ← IO.FS.Handle.mk lockFile .write
+    /-
+    Remark:
+    We do not wait for a lock here, because that can lead to deadlock.
+
+    This is because we are already holding a shared lock on the trace.
+    If multiple process race for this lock, one will get it and then
+    wait for an exclusive lock one the trace file, but be blocked by the
+    other process with a shared lock waiting on this file.
+
+    While there is likely a way to sequence this to avoid erroring,
+    simultaneous reconfigures are likely to produce unexpected results
+    anyway, so the error seems wise nonetheless.
+    -/
+    if (← hLock.tryLock) then
+      h.unlock
+      let h ← IO.FS.Handle.mk traceFile .readWrite
+      h.lock
+      hLock.unlock
+      return h
+    else
+      h.unlock
+      error <| s!"could not acquire an exclusive configuration lock; " ++
+        "another process may already be reconfiguring the package"
+  let configHash ← computeTextFileHash cfg.configFile
+  let elabConfig h (lakeOpts : NameMap String) : LogIO Environment := id do
+    /-
+    Remark:
+    We write the trace before elaborating the configuration file
+    to enable automatic reconfiguration on the next `lake` invocation if
+    elaboration fails. To ensure a failure triggers a reconfigure, we must also
+    remove any previous out-of-date `.olean`. Otherwise, Lake will treat the
+    older `.olean` as matching the new trace.
+
+    See the related PR and Zulip discussion for more details:
+    [leanprover/lean4#3069](https://github.com/leanprover/lean4/pull/3069).
+    -/
+    match (← IO.FS.removeFile olean |>.toBaseIO) with
+    | .ok _ | .error (.noFileOrDirectory ..) =>
+      h.putStrLn <| Json.pretty <| toJson
+        {platform := System.Platform.target, leanHash := cfg.lakeEnv.leanGithash,
+          configHash, options := lakeOpts : ConfigTrace}
+      h.truncate
+      let env ← elabConfigFile cfg.pkgDir lakeOpts cfg.leanOpts cfg.configFile
+      Lean.writeModule env olean
+      h.unlock
+      return env
+    | .error e => errorWithLog do
+      logError <| toString e
+      h.unlock
+      IO.FS.removeFile traceFile
+  let validateTrace h : LogIO Environment := id do
+    if cfg.reconfigure then
+      elabConfig (← acquireTrace h) cfg.lakeOpts
+    else
+      h.lock (exclusive := false)
+      let contents ← h.readToEnd
+      let .ok (trace : ConfigTrace) := Json.parse contents >>= fromJson?
+        | error "compiled configuration is invalid; run with '-R' to reconfigure"
+      let upToDate :=
+        (← olean.pathExists) ∧ trace.platform = System.Platform.target ∧
+        trace.leanHash = cfg.lakeEnv.leanGithash ∧ trace.configHash = configHash
+      if upToDate then
+        let env ← importConfigFileCore olean cfg.leanOpts
+        h.unlock
+        return env
+      else
+        elabConfig (← acquireTrace h) trace.options
+  if (← traceFile.pathExists) then
+    validateTrace <| ← IO.FS.Handle.mk traceFile .read
+  else
+    IO.FS.createDirAll cfg.lakeDir
+    match (← IO.FS.Handle.mk traceFile .writeNew |>.toBaseIO) with
+    | .ok h =>
+      h.lock; elabConfig h cfg.lakeOpts
+    | .error (.alreadyExists ..) =>
+      validateTrace <| ← IO.FS.Handle.mk traceFile .read
+    | .error e => error e.toString

backend/core/leanprover--lean4---v4.22.0/src/lean/lake/Lake/Load/Lean/Eval.lean

@@ -0,0 +1,186 @@
+/-
+Copyright (c) 2021 Mac Malone. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Mac Malone
+-/
+prelude
+import Lake.DSL.Attributes
+import Lake.Config.Workspace
+import Lean.DocString
+
+/-! # Lean Configuration Evaluator
+
+This module contains the definitions to load Lake configuration objects from
+a Lean environment elaborated from a Lake configuration file.
+-/
+
+open System Lean
+
+namespace Lake
+
+/-- Unsafe implementation of `evalConstCheck`. -/
+unsafe def unsafeEvalConstCheck
+  (env : Environment) (opts : Options) (α) [TypeName α] (const : Name)
+: Except String α :=
+  match env.find? const with
+  | none => throw s!"unknown constant '{const}'"
+  | some info =>
+    match info.type with
+    | Expr.const c _ =>
+      if c != TypeName.typeName α then
+        throwUnexpectedType
+      else
+        env.evalConst α opts const
+    | _ => throwUnexpectedType
+where
+  throwUnexpectedType : Except String α :=
+    throw s!"unexpected type at '{const}', `{TypeName.typeName α}` expected"
+
+/--
+Like `Lean.Environment.evalConstCheck`,
+but with plain universe-polymorphic `Except`.
+-/
+@[implemented_by unsafeEvalConstCheck]
+opaque evalConstCheck
+  (env : Environment) (opts : Options) (α) [TypeName α] (const : Name)
+: Except String α
+
+/-- Construct a `DNameMap` from the declarations tagged with `attr`. -/
+def mkTagMap
+  (env : Environment) (attr : OrderedTagAttribute)
+  [Monad m] (f : (n : Name) → m (β n))
+: m (DNameMap β) :=
+  let entries := attr.getAllEntries env
+  entries.foldlM (init := {}) fun map declName =>
+    return map.insert declName <| ← f declName
+
+/-- Construct a `OrdNameMap` from the declarations tagged with `attr`. -/
+def mkOrdTagMap
+  (env : Environment) (attr : OrderedTagAttribute)
+  [Monad m] (f : (n : Name) → m β)
+: m (OrdNameMap β) :=
+  let entries := attr.getAllEntries env
+  entries.foldlM (init := .mkEmpty entries.size) fun map declName =>
+    return map.insert declName <| ← f declName
+
+/-- Load a `PackageDecl` from a configuration environment. -/
+def PackageDecl.loadFromEnv
+  (env : Environment) (opts := Options.empty)
+: Except String PackageDecl := do
+  let declName ←
+    match packageAttr.getAllEntries env |>.toList with
+    | [] => error s!"configuration file is missing a `package` declaration"
+    | [name] => pure name
+    | _ => error s!"configuration file has multiple `package` declarations"
+  evalConstCheck env opts _ declName
+
+/--
+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.loadFromEnv
+  (self : Package) (env : Environment) (opts : Options)
+: LogIO Package := do
+  let strName := self.name.toString (escape := false)
+
+  -- load target, script, hook, and driver configurations
+  let constTargetMap ← IO.ofExcept <| mkOrdTagMap env targetAttr fun name => do
+    evalConstCheck env opts ConfigDecl name
+  let targetDecls ← constTargetMap.toArray.mapM fun decl => do
+    if h : decl.pkg = self.name then
+      return .mk decl h
+    else
+      error s!"\
+        target '{decl.name}' was defined in package '{decl.pkg}', \
+        but registered under '{self.name}'"
+  let targetDeclMap ← targetDecls.foldlM (init := {}) fun m decl => do
+    if let some orig := m.find? decl.name then
+      error s!"\
+        {self.name}: target '{decl.name}' was already defined as a '{orig.kind}', \
+        but then redefined as a '{decl.kind}'"
+    else
+      return m.insert decl.name (.mk decl rfl)
+  let defaultTargets ← defaultTargetAttr.getAllEntries env |>.mapM fun name =>
+    if let some decl := constTargetMap.find? name then pure decl.name else
+      error s!"{self.name}: package is missing target '{name}' marked as a default"
+  let scripts ← mkTagMap env scriptAttr fun scriptName => do
+    let name := strName ++ "/" ++ scriptName.toString (escape := false)
+    let fn ← IO.ofExcept <| evalConstCheck env opts ScriptFn scriptName
+    return {name, fn, doc? := ← findDocString? env scriptName : Script}
+  let defaultScripts ← defaultScriptAttr.getAllEntries env |>.mapM fun name =>
+    if let some script := scripts.find? name then pure script else
+      error s!"{self.name}: package is missing script '{name}' marked as a default"
+  let postUpdateHooks ← postUpdateAttr.getAllEntries env |>.mapM fun name =>
+    match evalConstCheck env opts PostUpdateHookDecl name with
+    | .ok decl =>
+      if h : decl.pkg = self.name then
+        return OpaquePostUpdateHook.mk ⟨h ▸ decl.fn⟩
+      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 name
+  let testDrivers ← testDriverAttr.getAllEntries env |>.mapM fun name =>
+    if let some decl := constTargetMap.find? name then
+      pure decl.name
+    else if scripts.contains name then
+      pure name
+    else
+      error s!"{self.name}: package is missing script or target '{name}' marked as a test driver"
+  let testDriver ←
+    if testDrivers.size > 1 then
+      error s!"{self.name}: only one script, executable, or library can be tagged @[test_driver]"
+    else if h : testDrivers.size > 0 then
+      if self.config.testDriver.isEmpty then
+        pure (testDrivers[0]'h |>.toString)
+      else
+        error s!"{self.name}: cannot both set testDriver and use @[test_driver]"
+    else
+      pure self.config.testDriver
+  let lintDrivers ← lintDriverAttr.getAllEntries env |>.mapM fun name =>
+    if let some decl := constTargetMap.find? name then
+      pure decl.name
+    else if scripts.contains name then
+      pure name
+    else
+      error s!"{self.name}: package is missing script or target '{name}' marked as a lint driver"
+  let lintDriver ←
+    if lintDrivers.size > 1 then
+      error s!"{self.name}: only one script or executable can be tagged @[lint_driver]"
+    else if h : lintDrivers.size > 0 then
+      if self.config.lintDriver.isEmpty then
+        pure (lintDrivers[0]'h |>.toString)
+      else
+        error s!"{self.name}: cannot both set lintDriver and use @[lint_driver]"
+    else
+      pure self.config.lintDriver
+
+  -- Deprecation warnings
+  unless self.config.manifestFile.isNone do
+    logWarning s!"{self.name}: package configuration option 'manifestFile' is deprecated"
+
+  -- Fill in the Package
+  return {self with
+    depConfigs, targetDecls, targetDeclMap
+    defaultTargets, scripts, defaultScripts
+    testDriver, lintDriver,  postUpdateHooks
+  }
+
+/--
+Load module/package facets into a `Workspace` from a configuration environment.
+-/
+def Workspace.addFacetsFromEnv
+  (env : Environment) (opts : Options) (self : Workspace)
+: Except String Workspace := do
+  let mut ws := self
+  for name in moduleFacetAttr.getAllEntries env do
+    let decl ← evalConstCheck env opts ModuleFacetDecl name
+    ws := ws.addModuleFacetConfig decl.config
+  for name in packageFacetAttr.getAllEntries env do
+    let decl ← evalConstCheck env opts PackageFacetDecl name
+    ws := ws.addPackageFacetConfig decl.config
+  for name in libraryFacetAttr.getAllEntries env do
+    let decl ← evalConstCheck env opts LibraryFacetDecl name
+    ws := ws.addLibraryFacetConfig decl.config
+  return ws

backend/core/leanprover--lean4---v4.22.0/src/lean/lake/Lake/Load/Manifest.lean

@@ -0,0 +1,290 @@
+/-
+Copyright (c) 2022 Mac Malone. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Mac Malone, Gabriel Ebner
+-/
+prelude
+import Lake.Util.Log
+import Lake.Util.Name
+import Lake.Util.FilePath
+import Lake.Util.JsonObject
+import Lake.Util.Version
+import Lake.Config.Defaults
+
+open System Lean
+
+/-! # Lake Manifest
+The data structure of a Lake manifest and the definitions needed
+to create, modify, serialize, and deserialize it.
+-/
+
+namespace Lake
+
+/--
+The current version of the manifest format.
+
+Three-part semantic versions were introduced in `v1.0.0`.
+Major version increments indicate breaking changes
+(e.g., new required fields and semantic changes to existing fields).
+Minor version increments (after `0.x`) indicate backwards-compatible extensions
+(e.g., adding optional fields, removing fields).
+
+Lake supports reading manifests with versions that have `-` suffixes.
+When checking for version compatibility, Lake expects a manifest with version
+`x.y.z-foo` to have all the features of the official manifest version `x.y.z`.
+That is, Lake ignores the `-` suffix.
+
+**VERSION HISTORY**
+
+**v0.x.0** (versioned by a natural number)
+- `1`: First version
+- `2`: Adds optional `inputRev` package entry field
+- `3`: Changes entry to inductive (with `path`/`git`)
+- `4`: Adds required `packagesDir` manifest field
+- `5`: Adds optional `inherited` package entry field (and removed `opts`)
+- `6`: Adds optional package root `name` manifest field
+- `7`: `type` refactor, custom to/fromJson
+
+**v1.x.x** (versioned by a string)
+- `"1.0.0"`: Switches to a semantic versioning scheme
+- `"1.1.0"`: Add optional `scope` package entry field
+-/
+@[inline] def Manifest.version : StdVer := {major := 1, minor := 1}
+
+/-- Manifest version `0.6.0` package entry. For backwards compatibility. -/
+inductive PackageEntryV6
+| path (name : Name) (opts : NameMap String) (inherited : Bool) (dir : FilePath)
+| git (name : Name) (opts : NameMap String) (inherited : Bool) (url : String) (rev : String)
+    (inputRev? : Option String) (subDir? : Option FilePath)
+deriving FromJson, ToJson, Inhabited
+
+/--
+The package source for an entry in the manifest.
+Describes exactly how Lake should materialize the package.
+-/
+inductive PackageEntrySrc
+  /--
+  A local filesystem package. `dir` is relative to the package directory
+  of the package containing the manifest.
+  -/
+  | path
+    (dir : FilePath)
+  /-- A remote Git package. -/
+  | git
+    (url : String)
+    (rev : String)
+    (inputRev? : Option String)
+    (subDir? : Option FilePath)
+  deriving Inhabited
+
+/-- An entry for a package stored in the manifest. -/
+structure PackageEntry where
+  name : Name
+  scope : String := ""
+  inherited : Bool
+  configFile : FilePath := defaultConfigFile
+  manifestFile? : Option FilePath := none
+  src : PackageEntrySrc
+  deriving Inhabited
+
+namespace PackageEntry
+
+protected def toJson (entry : PackageEntry) : Json :=
+  let fields := [
+    ("name", toJson entry.name),
+    ("scope", toJson entry.scope),
+    ("configFile" , toJson entry.configFile),
+    ("manifestFile", toJson entry.manifestFile?),
+    ("inherited", toJson entry.inherited),
+  ]
+  let fields :=
+    match entry.src with
+    | .path  dir =>
+      ("type", "path") :: fields.append [
+        ("dir", toJson dir),
+      ]
+    | .git url rev inputRev? subDir? =>
+      ("type", "git") :: fields.append [
+        ("url", toJson url),
+        ("rev", toJson rev),
+        ("inputRev", toJson inputRev?),
+        ("subDir", toJson subDir?),
+      ]
+  Json.mkObj fields
+
+instance : ToJson PackageEntry := ⟨PackageEntry.toJson⟩
+
+protected def fromJson? (json : Json) : Except String PackageEntry := do
+  let obj ← JsonObject.fromJson? json |>.mapError (s!"package entry: {·}")
+  let name ← obj.get "name" |>.mapError (s!"package entry: {·}")
+  let scope ← obj.getD "scope" ""
+  try
+    let type ← obj.get "type"
+    let inherited ← obj.get "inherited"
+    let configFile ← obj.getD "configFile" defaultConfigFile
+    let manifestFile ← obj.getD "manifestFile" defaultManifestFile
+    let src : PackageEntrySrc ← id do
+      match type with
+      | "path" =>
+        let dir ← obj.get "dir"
+        return .path dir
+      | "git" =>
+        let url ← obj.get "url"
+        let rev ← obj.get "rev"
+        let inputRev? ← obj.get? "inputRev"
+        let subDir? ← obj.get? "subDir"
+        return .git url rev inputRev? subDir?
+      | _ =>
+        throw s!"unknown package entry type '{type}'"
+    return {
+      name, scope, inherited,
+      configFile, manifestFile? := manifestFile, src
+      : PackageEntry
+    }
+  catch e =>
+    throw s!"package entry '{name}': {e}"
+
+instance : FromJson PackageEntry := ⟨PackageEntry.fromJson?⟩
+
+@[inline] def setInherited (entry : PackageEntry) : PackageEntry :=
+  {entry with inherited := true}
+
+@[inline] def setConfigFile (path : FilePath) (entry : PackageEntry) : PackageEntry :=
+  {entry with configFile := path}
+
+@[inline] def setManifestFile (path? : Option FilePath) (entry : PackageEntry) : PackageEntry :=
+  {entry with manifestFile? := path?}
+
+@[inline] def inDirectory (pkgDir : FilePath) (entry : PackageEntry) : PackageEntry :=
+  {entry with src := match entry.src with | .path dir => .path (pkgDir / dir) | s => s}
+
+def ofV6 : PackageEntryV6 → PackageEntry
+| .path name _opts inherited dir =>
+  {name, inherited, src := .path dir}
+| .git name _opts inherited url rev inputRev? subDir? =>
+  {name, inherited, src := .git url rev inputRev? subDir?}
+
+end PackageEntry
+
+/-- Manifest data structure that is serialized to the file. -/
+structure Manifest where
+  name : Name
+  lakeDir : FilePath
+  packagesDir? : Option FilePath := none
+  packages : Array PackageEntry := #[]
+
+namespace Manifest
+
+/-- Add a package entry to the end of a manifest. -/
+def addPackage (entry : PackageEntry) (self : Manifest) : Manifest :=
+  {self with packages := self.packages.push entry}
+
+protected def toJson (self : Manifest) : Json :=
+  Json.mkObj [
+    ("version", toJson version),
+    ("name", toJson self.name),
+    ("lakeDir", toJson self.lakeDir),
+    ("packagesDir", toJson self.packagesDir?),
+    ("packages", toJson self.packages),
+  ]
+
+instance : ToJson Manifest := ⟨Manifest.toJson⟩
+
+def getVersion (obj : JsonObject) : Except String SemVerCore := do
+  let ver : Json ← obj.get "version" <|> obj.get "schemaVersion"
+  let ver : SemVerCore ←
+    match ver with
+    | (n : Nat) => pure {minor := n}
+    | (s : String) => StdVer.parse s
+    | ver => throw s!"invalid version '{ver}'; \
+      you may need to update your 'lean-toolchain'"
+  if ver.major > 1 then
+    throw s!"schema version '{ver}' is of a higher major version than this \
+      Lake's '{Manifest.version}'; you may need to update your 'lean-toolchain'"
+  else if ver < {minor := 5} then
+    throw s!"incompatible manifest version '{ver}'"
+  else
+    return ver
+
+def getPackages (ver : StdVer) (obj : JsonObject) : Except String (Array PackageEntry) := do
+  if ver < {minor := 7} then
+    (·.map PackageEntry.ofV6) <$> obj.getD "packages" #[]
+  else
+    obj.getD "packages" #[]
+
+protected def fromJson? (json : Json) : Except String Manifest := do
+  let obj ← JsonObject.fromJson? json
+  let ver ← getVersion obj
+  let name ← obj.getD "name" Name.anonymous
+  let lakeDir ← obj.getD "lakeDir" defaultLakeDir
+  let packagesDir? ← obj.get? "packagesDir"
+  let packages ← getPackages ver obj
+  return {name, lakeDir, packagesDir?, packages}
+
+instance : FromJson Manifest := ⟨Manifest.fromJson?⟩
+
+/-- Parse a `Manifest` from a string. -/
+def parse (data : String) : Except String Manifest := do
+  match Json.parse data with
+  | .ok json => fromJson? json
+  | .error e => throw s!"invalid JSON: {e}"
+
+/-- Parse a manifest file. -/
+def load (file : FilePath) : IO Manifest := do
+  let contents ← IO.FS.readFile file
+  match inline <| Manifest.parse contents with
+  | .ok a => return a
+  | .error e => error s!"{file}: {e}"
+
+/--
+Parse a manifest file. Returns `none` if the file does not exist.
+Errors if the manifest is ill-formatted or the read files for other reasons.
+-/
+def load? (file : FilePath) : IO (Option Manifest) := do
+  match (← inline (load file) |>.toBaseIO) with
+  | .ok contents => return contents
+  | .error (.noFileOrDirectory ..) => return none
+  | .error e => throw e
+
+/-- Serialize the manifest to a JSON file. -/
+def save (self : Manifest) (manifestFile : FilePath) : IO PUnit := do
+  let contents := Json.pretty self.toJson
+  IO.FS.writeFile manifestFile <| contents.push '\n'
+
+@[deprecated save (since := "2024-12-17")] abbrev saveToFile := @save
+
+/-- Deserialize package entries from a (partial) JSON manifest. -/
+def decodeEntries (data : Json)  : Except String (Array PackageEntry) := do
+  let obj ← JsonObject.fromJson? data
+  getPackages (← getVersion obj) obj
+
+/-- Deserialize manifest package entries from a JSON string. -/
+def parseEntries (data : String) : Except String (Array PackageEntry) := do
+  match Json.parse data with
+  | .ok json => decodeEntries json
+  | .error e => throw s!"invalid JSON: {e}"
+
+/-- Deserialize manifest package entries from a JSON file. -/
+def loadEntries (file : FilePath) : IO (Array PackageEntry) := do
+  let contents ← IO.FS.readFile file
+  match inline <| parseEntries contents with
+  | .ok a => return a
+  | .error e => error s!"{file}: {e}"
+
+/--
+Deserialize manifest package entries from a JSON file.
+Returns an empty array if the file does not exist.
+-/
+def tryLoadEntries (file : FilePath) : IO (Array PackageEntry) := do
+  match  (← inline (loadEntries file) |>.toBaseIO) with
+  | .ok a => return a
+  | .error (.noFileOrDirectory ..) => return #[]
+  | .error e => error s!"{file}: {e}"
+
+/-- Serialize manifest package entries to a JSON file. -/
+def saveEntries (file : FilePath) (entries : Array PackageEntry)  : IO PUnit := do
+  let contents := Json.pretty <| Json.mkObj [
+    ("schemaVersion", toJson version),
+    ("packages", toJson entries)
+  ]
+  IO.FS.writeFile file <| contents.push '\n'

backend/core/leanprover--lean4---v4.22.0/src/lean/lake/Lake/Load/Materialize.lean

@@ -0,0 +1,216 @@
+/-
+Copyright (c) 2017 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Gabriel Ebner, Sebastian Ullrich, Mac Malone
+-/
+prelude
+import Lake.Util.Git
+import Lake.Load.Manifest
+import Lake.Config.Dependency
+import Lake.Config.Package
+import Lake.Reservoir
+
+open System Lean
+
+/-! # Dependency Materialization
+Definitions to "materialize" a package dependency.
+That is, clone a local copy of a Git dependency at a specific revision
+or resolve a local path dependency.
+-/
+
+namespace Lake
+
+/-- Update the Git package in `repo` to `rev` if not already at it. -/
+def updateGitPkg
+  (name : String) (repo : GitRepo) (rev? : Option String)
+: LogIO PUnit := do
+  let rev ← repo.findRemoteRevision rev?
+  if (← repo.getHeadRevision) = rev then
+    if (← repo.hasDiff) then
+      logWarning s!"{name}: repository '{repo.dir}' has local changes"
+  else
+    logInfo s!"{name}: checking out revision '{rev}'"
+    repo.checkoutDetach rev
+
+/-- Clone the Git package as `repo`. -/
+def cloneGitPkg
+  (name : String) (repo : GitRepo) (url : String) (rev? : Option String)
+: LogIO PUnit := do
+  logInfo s!"{name}: cloning {url}"
+  repo.clone url
+  if let some rev := rev? then
+    let rev ← repo.resolveRemoteRevision rev
+    logInfo s!"{name}: checking out revision '{rev}'"
+    repo.checkoutDetach rev
+
+/--
+Update the Git repository from `url` in `repo` to `rev?`.
+If `repo` is already from `url`, just checkout the new revision.
+Otherwise, delete the local repository and clone a fresh copy from `url`.
+-/
+def updateGitRepo
+  (name : String) (repo : GitRepo) (url : String) (rev? : Option String)
+: LogIO Unit := do
+  let sameUrl ← EIO.catchExceptions (h := fun _ => pure false) <| show IO Bool from do
+    let some remoteUrl ← repo.getRemoteUrl? | return false
+    if remoteUrl = url then return true
+    return (← IO.FS.realPath remoteUrl) = (← IO.FS.realPath url)
+  if sameUrl then
+    updateGitPkg name repo rev?
+  else
+    if System.Platform.isWindows then
+      -- Deleting git repositories via IO.FS.removeDirAll does not work reliably on windows
+      logInfo s!"{name}: URL has changed; you might need to delete '{repo.dir}' manually"
+      updateGitPkg name repo rev?
+    else
+      logInfo s!"{name}: URL has changed; deleting '{repo.dir}' and cloning again"
+      IO.FS.removeDirAll repo.dir
+      cloneGitPkg name repo url rev?
+
+/--
+Materialize the Git repository from `url` into `repo` at `rev?`.
+Clone it if no local copy exists, otherwise update it.
+-/
+def materializeGitRepo
+  (name : String) (repo : GitRepo) (url : String) (rev? : Option String)
+: LogIO Unit := do
+  if (← repo.dirExists) then
+    updateGitRepo name repo url rev?
+  else
+    cloneGitPkg name repo url rev?
+
+structure MaterializedDep where
+  /-- Path to the materialized package relative to the workspace's root directory. -/
+  relPkgDir : FilePath
+  /--
+  URL for the materialized package.
+  Used as the endpoint from which to fetch cloud releases for the package.
+  -/
+  remoteUrl : String
+  /-- The manifest entry for the dependency. -/
+  manifestEntry : PackageEntry
+  deriving Inhabited
+
+@[inline] def MaterializedDep.name (self : MaterializedDep) :=
+  self.manifestEntry.name
+
+@[inline] def MaterializedDep.scope (self : MaterializedDep) :=
+  self.manifestEntry.scope
+
+/-- Path to the dependency's configuration file (relative to `relPkgDir`). -/
+@[inline] def MaterializedDep.manifestFile? (self : MaterializedDep) :=
+  self.manifestEntry.manifestFile?
+
+/-- Path to the dependency's configuration file (relative to `relPkgDir`). -/
+@[inline] def MaterializedDep.configFile (self : MaterializedDep) :=
+  self.manifestEntry.configFile
+
+def pkgNotIndexed (scope name : String) (rev? : Option String := none) : String :=
+  let (leanRev, tomlRev) :=
+    if let some rev := rev? then
+      (s!" @ {repr rev}", s! "\n    rev = {repr rev}")
+    else ("", "")
+s!"{scope}/{name}: package not found on Reservoir.
+
+  If the package is on GitHub, you can add a Git source. For example:
+
+    require ...
+      from git \"https://github.com/{scope}/{name}\"{leanRev}
+
+  or, if using TOML:
+
+    [[require]]
+    git = \"https://github.com/{scope}/{name}\"{tomlRev}
+    ...
+"
+
+/--
+Materializes a configuration dependency.
+For Git dependencies, updates it to the latest input revision.
+-/
+def Dependency.materialize
+  (dep : Dependency) (inherited : Bool)
+  (lakeEnv : Env) (wsDir relPkgsDir relParentDir : FilePath)
+: LogIO MaterializedDep := do
+  if let some src := dep.src? then
+    match src with
+    | .path dir =>
+      let relPkgDir := relParentDir / dir
+      return mkDep relPkgDir "" (.path relPkgDir)
+    | .git url inputRev? subDir? => do
+      let sname := dep.name.toString (escape := false)
+      let repoUrl := Git.filterUrl? url |>.getD ""
+      materializeGit sname (relPkgsDir / sname) url repoUrl inputRev? subDir?
+  else
+    if dep.scope.isEmpty then
+      error s!"{dep.name}: ill-formed dependency: \
+        dependency is missing a source and is missing a scope for Reservoir"
+    let verRev? ← dep.version?.mapM fun ver =>
+      if ver.startsWith "git#" then
+        return ver.drop 4
+      else
+        error s!"{dep.name}: unsupported dependency version format '{ver}' (should be \"git#<rev>\")"
+    let depName := dep.name.toString (escape := false)
+    let pkg ←
+      match (← Reservoir.fetchPkg? lakeEnv dep.scope depName |>.toLogT) with
+      | .ok (some pkg) => pure pkg
+      | .ok none => error <| pkgNotIndexed dep.scope depName verRev?
+      | .error e =>
+          logError s!"{dep.scope}/{depName}: could not materialize package: \
+            this may be a transient error or a bug in Lake or Reservoir"
+          throw e
+    let relPkgDir := relPkgsDir / pkg.name
+    match pkg.gitSrc? with
+    | some (.git _ url githubUrl? defaultBranch? subDir?) =>
+      materializeGit pkg.fullName relPkgDir url
+        (githubUrl?.getD "") (verRev? <|> defaultBranch?) subDir?
+    | _ => error s!"{pkg.fullName}: Git source not found on Reservoir"
+where
+  materializeGit name relPkgDir gitUrl remoteUrl inputRev? subDir? : LogIO MaterializedDep := do
+    let repo := GitRepo.mk (wsDir / relPkgDir)
+    let gitUrl := lakeEnv.pkgUrlMap.find? dep.name |>.getD gitUrl
+    materializeGitRepo name repo gitUrl inputRev?
+    let rev ← repo.getHeadRevision
+    let relPkgDir := if let some subDir := subDir? then relPkgDir / subDir else relPkgDir
+    return mkDep relPkgDir remoteUrl <| .git gitUrl rev inputRev? subDir?
+  @[inline] mkDep relPkgDir remoteUrl src : MaterializedDep := {
+    relPkgDir, remoteUrl,
+    manifestEntry := {name := dep.name, scope := dep.scope, inherited, src}
+  }
+
+/--
+Materializes a manifest package entry, cloning and/or checking it out as necessary.
+-/
+def PackageEntry.materialize
+  (manifestEntry : PackageEntry)
+  (lakeEnv : Env) (wsDir relPkgsDir : FilePath)
+: LogIO MaterializedDep :=
+  match manifestEntry.src with
+  | .path (dir := relPkgDir) .. =>
+    return mkDep relPkgDir ""
+  | .git (url := url) (rev := rev) (subDir? := subDir?) .. => do
+    let sname := manifestEntry.name.toString (escape := false)
+    let relGitDir := relPkgsDir / sname
+    let gitDir := wsDir / relGitDir
+    let repo := GitRepo.mk gitDir
+    /-
+    Do not update (fetch remote) if already on revision
+    Avoids errors when offline, e.g., [leanprover/lake#104][104].
+
+    [104]: https://github.com/leanprover/lake/issues/104
+    -/
+    if (← repo.dirExists) then
+      if (← repo.getHeadRevision?) = rev then
+        if (← repo.hasDiff) then
+          logWarning s!"{sname}: repository '{repo.dir}' has local changes"
+      else
+        let url := lakeEnv.pkgUrlMap.find? manifestEntry.name |>.getD url
+        updateGitRepo sname repo url rev
+    else
+      let url := lakeEnv.pkgUrlMap.find? manifestEntry.name |>.getD url
+      cloneGitPkg sname repo url rev
+    let relPkgDir := match subDir? with | .some subDir => relGitDir / subDir | .none => relGitDir
+    return mkDep relPkgDir (Git.filterUrl? url |>.getD "")
+where
+  @[inline] mkDep relPkgDir remoteUrl : MaterializedDep :=
+    {relPkgDir, remoteUrl, manifestEntry}

backend/core/leanprover--lean4---v4.22.0/src/lean/lake/Lake/Load/Package.lean

@@ -0,0 +1,92 @@
+/-
+Copyright (c) 2024 Mac Malone. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Mac Malone
+-/
+prelude
+import Lake.Load.Lean
+import Lake.Load.Toml
+
+/-! # Package Loader
+
+This module contains the main definitions to load a package
+from Lake configuration file (either Lean or TOML).
+-/
+
+open Lean
+
+namespace Lake
+open System (FilePath)
+
+/--
+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
+
+/--
+Returns the normalized real path of the configuration file (if it exists).
+Otherwise, returns an empty string.
+-/
+def realConfigFile (cfgFile : FilePath) : BaseIO FilePath := do
+  if cfgFile.extension.isSome then
+    resolvePath cfgFile
+  else
+    if let some path ← resolvePath? (cfgFile.addExtension "lean") then
+      return path
+    else
+      resolvePath (cfgFile.addExtension "toml")
+
+/--
+Loads a Lake package configuration (either Lean or TOML).
+The resulting package does not yet include any dependencies.
+-/
+def loadPackageCore
+  (name : String) (cfg : LoadConfig)
+: LogIO (Package × Option Environment) := do
+  if let some ext := cfg.relConfigFile.extension then
+    let cfg ←
+      if let some configFile ← resolvePath? cfg.configFile then
+        pure {cfg with configFile}
+      else error s!"{name}: configuration file not found: {cfg.configFile}"
+    match ext with
+    | "lean" => (·.map id some) <$> loadLeanConfig cfg
+    | "toml" => ((·,none)) <$> loadTomlConfig cfg
+    | _ => 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
+    if let some configFile ← resolvePath? leanFile then
+      if (← tomlFile.pathExists) then
+        logInfo s!"{name}: {relLeanFile} and {relTomlFile} are both present; using {relLeanFile}"
+       let cfg := {cfg with configFile, relConfigFile := relLeanFile}
+      let (pkg, env) ← loadLeanConfig cfg
+      return (pkg, some env)
+    else
+      if let some configFile ← resolvePath? tomlFile then
+        let cfg := {cfg with configFile, relConfigFile := relTomlFile}
+        let pkg ← loadTomlConfig cfg
+        return (pkg, none)
+      else
+        error s!"{name}: no configuration file with a supported extension:\n{leanFile}\n{tomlFile}"
+
+/-- Loads a Lake package as a single independent object (without dependencies). -/
+def loadPackage (config : LoadConfig) : LogIO Package := do
+  Lean.searchPathRef.set config.lakeEnv.leanSearchPath
+  (·.1) <$> loadPackageCore "[root]" config
+
+/-- Load the package's input-to-content mapping from the Lake cache (if enabled). -/
+protected def Package.loadInputsFrom (env : Env) (pkg : Package) : LogIO Package := do
+  if env.lakeCache.isDisabled || !(pkg.enableArtifactCache?.getD env.enableArtifactCache) then
+    return pkg
+  else
+    let inputs ← CacheMap.load (pkg.inputsFileIn env.lakeCache)
+    return {pkg with cacheRef? := ← IO.mkRef inputs}

backend/core/leanprover--lean4---v4.22.0/src/lean/lake/Lake/Load/Resolve.lean

@@ -0,0 +1,471 @@
+/-
+Copyright (c) 2022 Mac Malone. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Mac Malone, Gabriel Ebner
+-/
+prelude
+import Lake.Config.Monad
+import Lake.Util.StoreInsts
+import Lake.Build.Topological
+import Lake.Load.Materialize
+import Lake.Load.Package
+
+open System Lean
+
+/-! # Dependency Resolution
+
+This module contains definitions for resolving the dependencies of a package.
+-/
+
+namespace Lake
+
+def stdMismatchError (newName : String) (rev : String) :=
+s!"the 'std' package has been renamed to '{newName}' and moved to the
+'leanprover-community' organization; downstream packages which wish to
+update to the new std should replace
+
+  require std from
+    git \"https://github.com/leanprover/std4\"{rev}
+
+in their Lake configuration file with
+
+  require {newName} from
+    git \"https://github.com/leanprover-community/{newName}\"{rev}
+"
+
+/--
+Loads the package configuration of a materialized dependency.
+Adds the facets defined in the package to the `Workspace`.
+-/
+def loadDepPackage
+  (dep : MaterializedDep)
+  (lakeOpts : NameMap String)
+  (leanOpts : Options) (reconfigure : Bool)
+: StateT Workspace LogIO Package := fun ws => do
+  let name := dep.name.toString (escape := false)
+  let pkgDir := ws.dir / dep.relPkgDir
+  let some pkgDir ← resolvePath? pkgDir
+    | error s!"{name}: package directory not found: {pkgDir}"
+  let (pkg, env?) ← loadPackageCore name {
+    lakeEnv := ws.lakeEnv
+    wsDir := ws.dir
+    pkgDir
+    relPkgDir := dep.relPkgDir
+    relConfigFile := dep.configFile
+    lakeOpts, leanOpts, reconfigure
+    scope := dep.scope
+    remoteUrl := dep.remoteUrl
+  }
+  let pkg ← pkg.loadInputsFrom ws.lakeEnv
+  if let some env := env? then
+    let ws ← IO.ofExcept <| ws.addFacetsFromEnv env leanOpts
+    return (pkg, ws)
+  else
+    return (pkg, ws)
+
+/--
+The resolver's call stack of dependencies.
+That is, the dependency currently being resolved plus its parents.
+-/
+abbrev DepStack := CallStack Name
+
+/--
+A monad transformer for recursive dependency resolution.
+It equips the monad with the stack of dependencies currently being resolved.
+-/
+abbrev DepStackT m := CallStackT Name m
+
+@[inline] nonrec def DepStackT.run
+  (x : DepStackT m α) (stack : DepStack := {})
+: m α :=
+  x.run stack
+
+/-- Log dependency cycle and error. -/
+@[specialize] def depCycleError [MonadError m] (cycle : Cycle Name) : m α :=
+  error s!"dependency cycle detected:\n{formatCycle cycle}"
+
+instance [Monad m] [MonadError m] : MonadCycleOf Name (DepStackT m) where
+  throwCycle := depCycleError
+
+/-- The monad of the dependency resolver. -/
+abbrev ResolveT m := DepStackT <| StateT Workspace m
+
+@[inline] nonrec def ResolveT.run
+  (ws : Workspace) (x : ResolveT m α) (stack : DepStack := {})
+: m (α × Workspace) :=
+  x.run stack |>.run ws
+
+/-- Recursively run a `ResolveT` monad starting from the workspace's root. -/
+@[specialize] private def Workspace.runResolveT
+  [Monad m] [MonadError m] (ws : Workspace)
+  (go : RecFetchFn Package PUnit (ResolveT m))
+  (root := ws.root) (stack : DepStack  := {})
+: m Workspace := do
+  let (_, ws) ← ResolveT.run ws (stack := stack) do
+    inline <| recFetchAcyclic (·.name) go root
+  return ws
+
+/-
+Recursively visits each node in a package's dependency graph, starting from
+the workspace package `root`. Each dependency missing from the workspace is
+resolved using the `resolve` function and added into the workspace.
+
+Recursion occurs breadth-first. Each direct dependency of a package is
+resolved in reverse order before recursing to the dependencies' dependencies.
+
+See `Workspace.updateAndMaterializeCore` for more details.
+-/
+@[inline] private def Workspace.resolveDepsCore
+  [Monad m] [MonadError m] (ws : Workspace)
+  (load : Package → Dependency → StateT Workspace m Package)
+  (root : Package := ws.root) (stack : DepStack := {})
+: m Workspace := do
+  ws.runResolveT go root stack
+where
+  @[specialize] go pkg recurse : ResolveT m Unit := do
+    let start := (← getWorkspace).packages.size
+    -- Materialize and load the missing direct dependencies of `pkg`
+    pkg.depConfigs.forRevM fun dep => do
+      let ws ← getWorkspace
+      if ws.packageMap.contains dep.name then
+        return -- already handled in another branch
+      if pkg.name = dep.name then
+        error s!"{pkg.name}: package requires itself (or a package with the same name)"
+      let depPkg ← load pkg dep
+      modifyThe Workspace (·.addPackage depPkg)
+    -- Recursively load the dependencies' dependencies
+    (← getWorkspace).packages.forM recurse start
+
+/--
+Adds monad state used to update the manifest.
+It equips the monad with a map of locked dependencies.
+-/
+abbrev UpdateT := StateT (NameMap PackageEntry)
+
+@[inline] nonrec def UpdateT.run (x : UpdateT m α) (init : NameMap PackageEntry := {}) : m (α × NameMap PackageEntry) :=
+  x.run init
+
+/--
+Reuse manifest versions of root packages that should not be updated.
+Also, move the packages directory if its location has changed.
+-/
+private def reuseManifest
+  (ws : Workspace) (toUpdate : NameSet)
+: UpdateT LoggerIO PUnit := do
+  let rootName := ws.root.name.toString (escape := false)
+  match (← Manifest.load ws.manifestFile |>.toBaseIO) with
+  | .ok manifest =>
+    -- Reuse manifest versions
+    unless toUpdate.isEmpty do
+      manifest.packages.forM fun entry => do
+        unless entry.inherited || toUpdate.contains entry.name do
+          store entry.name entry
+    -- Move packages directory
+    if let some oldRelPkgsDir := manifest.packagesDir? then
+      let oldPkgsDir := ws.dir / oldRelPkgsDir
+      if oldRelPkgsDir.normalize != ws.relPkgsDir.normalize && (← oldPkgsDir.pathExists) then
+        logInfo s!"workspace packages directory changed; \
+          renaming '{oldPkgsDir}' to '{ws.pkgsDir}'"
+        let doRename : IO Unit := do
+          createParentDirs ws.pkgsDir
+          IO.FS.rename oldPkgsDir ws.pkgsDir
+        if let .error e ← doRename.toBaseIO then
+          error s!"could not rename workspace packages directory: {e}"
+  | .error (.noFileOrDirectory ..) =>
+    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!"{rootName}: ignoring previous manifest because it failed to load: {e}"
+
+/-- Add a package dependency's manifest entries to the update state. -/
+private def addDependencyEntries (pkg : Package) : UpdateT LoggerIO PUnit := do
+  match (← Manifest.load pkg.manifestFile |>.toBaseIO) with
+  | .ok manifest =>
+    manifest.packages.forM fun entry => do
+      unless (← getThe (NameMap PackageEntry)).contains entry.name do
+        let entry := entry.setInherited.inDirectory pkg.relDir
+        store entry.name entry
+  | .error (.noFileOrDirectory ..) =>
+    logWarning s!"{pkg.name}: ignoring missing manifest '{pkg.manifestFile}'"
+  | .error e =>
+    logWarning s!"{pkg.name}: ignoring manifest because it failed to load: {e}"
+
+/-- Materialize a single dependency, updating it if desired. -/
+private def updateAndMaterializeDep
+  (ws : Workspace) (pkg : Package) (dep : Dependency)
+: UpdateT LoggerIO MaterializedDep := do
+  if let some entry ← fetch? dep.name then
+    entry.materialize ws.lakeEnv ws.dir ws.relPkgsDir
+  else
+    let inherited := pkg.name ≠ ws.root.name
+    /-
+    NOTE: A path dependency inherited from another dependency's manifest
+    will always be of the form a `./<relPath>` (i.e., be relative to its
+    workspace).  Thus, when relativized to this workspace, it will have the
+    path  `<relPkgDir>/./<relPath>`. However, if defining dependency lacks
+    a manifest, it will instead be locked as `<relPkgDir>/<relPath>`.
+    Adding a `.` here eliminates this difference.
+    -/
+    let relPkgDir := if pkg.relDir == "." then pkg.relDir else pkg.relDir / "."
+    let matDep ← dep.materialize inherited ws.lakeEnv ws.dir ws.relPkgsDir relPkgDir
+    store matDep.name matDep.manifestEntry
+    return matDep
+
+/-- Verify that a dependency was loaded with the correct name. -/
+private def validateDep
+  (pkg : Package) (dep : Dependency) (matDep : MaterializedDep) (depPkg : Package)
+: LoggerIO PUnit := do
+  if depPkg.name ≠ dep.name then
+    if dep.name = .mkSimple "std" then
+      let rev :=
+        match matDep.manifestEntry.src with
+        | .git (inputRev? := some rev) .. => s!" @ {repr rev}"
+        | _ => ""
+      logError (stdMismatchError depPkg.name.toString rev)
+    if matDep.manifestEntry.src matches .git .. then
+      if let .error e ← IO.FS.removeDirAll depPkg.dir |>.toBaseIO then -- cleanup
+        -- Deleting git repositories via IO.FS.removeDirAll does not work reliably on Windows
+        logError s!"'{dep.name}' was downloaded incorrectly; \
+          you will need to manually delete '{depPkg.dir}': {e}"
+    error s!"{pkg.name}: package '{depPkg.name}' was required as '{dep.name}'"
+
+/--
+Exit code returned if Lake needs a manual restart.
+Used, for instance, if the toolchain is updated and no Elan is detected.
+-/
+def restartCode : ExitCode := 4
+
+/--
+Update the workspace's `lean-toolchain` if necessary.
+
+Compares the root's toolchain with that of its direct dependencies to find the
+best match. If none can be found, issue warning and return normally. If an
+update is found
+-/
+def Workspace.updateToolchain
+  (ws : Workspace) (rootDeps : Array MaterializedDep)
+: LoggerIO PUnit := do
+  let rootToolchainFile := ws.root.dir / toolchainFileName
+  let rootTc? ← ToolchainVer.ofDir? ws.dir
+  let (src, tc?, tcs) ← rootDeps.foldlM (init := (ws.root.name, rootTc?, #[])) fun s dep => do
+    let depTc? ← ToolchainVer.ofDir? (ws.dir / dep.relPkgDir)
+    let some depTc := depTc?
+      | return s
+    let (src, tc?, tcs) := s
+    let some tc := tc?
+      | return (dep.name, depTc?, tcs)
+    if depTc ≤ tc then
+      return (src, tc, tcs)
+    else if tc < depTc then
+      return (dep.name, depTc, tcs)
+    else
+      return (src, tc, tcs.push (dep.name, depTc))
+  if 0 < tcs.size then
+    let s := "toolchain not updated; multiple toolchain candidates:"
+    let s := if let some tc := tc? then s!"{s}\n  {tc}\n    from {src}" else s
+    let s := tcs.foldl (init := s) fun s (d, tc) => s!"{s}\n  {tc}\n    from {d}"
+    logWarning s
+  else if let some tc := tc? then
+    if rootTc?.any (· == tc) then
+      logInfo "toolchain not updated; already up-to-date"
+      return
+    logInfo s!"updating toolchain to '{tc}'"
+    IO.FS.writeFile rootToolchainFile tc.toString
+    let some lakeArgs := ws.lakeArgs?
+      | logInfo s!"cannot auto-restart; you will need to manually restart Lake"
+        IO.Process.exit restartCode.toUInt8
+    let some elanInstall := ws.lakeEnv.elan?
+      | logInfo s!"no Elan detected; you will need to manually restart Lake"
+        IO.Process.exit restartCode.toUInt8
+    logInfo s!"restarting Lake via Elan"
+    let child ← IO.Process.spawn {
+      cmd := elanInstall.elan.toString
+      args := #["run", "--install", tc.toString, "lake"] ++ lakeArgs
+      env := Env.noToolchainVars
+    }
+    IO.Process.exit (← child.wait).toUInt8
+  else
+    logInfo s!"toolchain not updated; no toolchain information found"
+
+/--
+Updates the workspace, materializing and reconfiguring dependencies.
+
+Dependencies are updated to latest specific revision matching that in `require`
+(e.g., if the `require` is `@master`, update to latest commit on master) or
+removed if the `require` is removed.
+If `tuUpdate` is empty, all direct dependencies of the workspace's root will be
+updated and/or remove. Otherwise, only those specified will be updated.
+
+If `updateToolchain := true`, the workspace's toolchain is also updated to the
+latest toolchain compatible with the root and its direct dependencies.
+If there are multiple incomparable toolchain versions across them,
+a warning will be issued and no update performed.
+If an update is performed, Lake will automatically restart the update on the new
+toolchain (via `elan`). If `elan` is missing, it will instead request a manual
+restart from the user and exit immediately with `restartCode`.
+
+**Dependency Traversal Order**
+
+All dependencies of a package are visited in reverse order before recursing
+to the dependencies' dependencies. For example, given the dependency graph:
+
+```
+R
+|- A
+|- B
+ |- X
+ |- Y
+|- C
+```
+
+Lake follows the order `R`, `C`, `B`, `A`, `Y`, `X`.
+
+The reason for this is two-fold:
+1. Like targets, later requires should shadow earlier definitions.
+2. Requires written by a user should take priority over those inherited
+from dependencies.
+
+Were Lake to use a depth-first traversal, for example, Lake would follow
+the order `R`, `A`, `B`, `X`, `Y`, `C`. If `X` and `C` are both the package
+`foo`, Lake would use the configuration of `foo` found in `B` rather than in
+the root `R`, which would likely confuse the user.
+-/
+def Workspace.updateAndMaterializeCore
+  (ws : Workspace)
+  (toUpdate : NameSet := {}) (leanOpts : Options := {})
+  (updateToolchain := true)
+: LoggerIO (Workspace × NameMap PackageEntry) := UpdateT.run do
+  reuseManifest ws toUpdate
+  let ws := ws.addPackage ws.root
+  if updateToolchain then
+    let deps := ws.root.depConfigs.reverse
+    let matDeps ← deps.mapM fun dep => do
+      logVerbose s!"{ws.root.name}: updating '{dep.name}' with {toJson dep.opts}"
+      updateAndMaterializeDep ws ws.root dep
+    ws.updateToolchain matDeps
+    let start := ws.packages.size
+    let ws ← (deps.zip matDeps).foldlM (init := ws) fun ws (dep, matDep) => do
+      let (depPkg, ws) ← loadUpdatedDep ws.root dep matDep ws
+      let ws := ws.addPackage depPkg
+      return ws
+    ws.packages.foldlM (init := ws) (start := start) fun ws pkg =>
+      ws.resolveDepsCore (stack := [ws.root.name]) updateAndLoadDep pkg
+  else
+    ws.resolveDepsCore updateAndLoadDep
+where
+  @[inline] updateAndLoadDep pkg dep := do
+    let matDep ← updateAndMaterializeDep (← getWorkspace) pkg dep
+    loadUpdatedDep pkg dep matDep
+  @[inline] loadUpdatedDep pkg dep matDep : StateT Workspace (UpdateT LoggerIO) Package  := do
+    let depPkg ← loadDepPackage matDep dep.opts leanOpts true
+    validateDep pkg dep matDep depPkg
+    addDependencyEntries depPkg
+    return depPkg
+
+/-- Write package entries to the workspace manifest. -/
+def Workspace.writeManifest
+  (ws : Workspace) (entries : NameMap PackageEntry)
+: IO PUnit := do
+  let manifestEntries := ws.packages.foldl (init := #[]) fun arr pkg =>
+    match entries.find? pkg.name with
+    | some entry => arr.push <|
+      entry.setManifestFile pkg.relManifestFile |>.setConfigFile pkg.relConfigFile
+    | none => arr -- should only be the case for the root
+  let manifest : Manifest := {
+    name := ws.root.name
+    lakeDir := ws.relLakeDir
+    packagesDir? := ws.relPkgsDir
+    packages := manifestEntries
+  }
+  manifest.save ws.manifestFile
+
+/-- Run a package's `post_update` hooks. -/
+def Package.runPostUpdateHooks (pkg : Package) : LakeT LoggerIO PUnit := do
+  unless pkg.postUpdateHooks.isEmpty do
+  logInfo s!"{pkg.name}: running post-update hooks"
+  pkg.postUpdateHooks.forM fun hook => hook.get.fn pkg
+
+/--
+Updates the workspace, writes the new Lake manifest, and runs package
+post-update hooks.
+
+See `Workspace.updateAndMaterializeCore` for details on the update process.
+-/
+def Workspace.updateAndMaterialize
+  (ws : Workspace)
+  (toUpdate : NameSet := {}) (leanOpts : Options := {})
+  (updateToolchain := true)
+: LoggerIO Workspace := do
+  let (ws, entries) ←
+    ws.updateAndMaterializeCore toUpdate leanOpts updateToolchain
+  ws.writeManifest entries
+  ws.runLakeT do ws.packages.forM (·.runPostUpdateHooks)
+  return ws
+
+/--
+Check whether entries in the manifest are up-to-date,
+reporting warnings and/or errors as appropriate.
+-/
+def validateManifest
+  (pkgEntries : NameMap PackageEntry) (deps : Array Dependency)
+: LoggerIO PUnit := do
+  deps.forM fun dep => do
+    let warnOutOfDate (what : String) :=
+      logWarning <|
+        s!"manifest out of date: {what} of dependency '{dep.name}' changed; \
+        use `lake update {dep.name}` to update it"
+    let some src := dep.src? | return
+    let some entry := pkgEntries.find? dep.name | return
+    match src, entry.src with
+    | .git (url := url) (rev := rev) .., .git (url := url') (inputRev? := rev')  .. =>
+      if url ≠ url' then warnOutOfDate "git url"
+      if rev ≠ rev' then warnOutOfDate "git revision"
+    | .path .., .path .. => pure ()
+    | _, _ => warnOutOfDate "source kind (git/path)"
+
+/--
+Resolving a workspace's dependencies using a manifest,
+downloading and/or updating them as necessary.
+-/
+def Workspace.materializeDeps
+  (ws : Workspace) (manifest : Manifest)
+  (leanOpts : Options := {}) (reconfigure := false)
+  (overrides : Array PackageEntry := #[])
+: LoggerIO Workspace := do
+  -- Load locked dependencies
+  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 mut pkgEntries := mkNameMap PackageEntry
+  pkgEntries := manifest.packages.foldl (init := pkgEntries) fun map entry =>
+    map.insert entry.name entry
+  validateManifest pkgEntries ws.root.depConfigs
+  let wsOverrides ← Manifest.tryLoadEntries ws.packageOverridesFile
+  pkgEntries := wsOverrides.foldl (init := pkgEntries) fun map entry =>
+    map.insert entry.name entry
+  pkgEntries := overrides.foldl (init := pkgEntries) fun map entry =>
+    map.insert entry.name entry
+  if pkgEntries.isEmpty && !ws.root.depConfigs.isEmpty then
+    error "missing manifest; use `lake update` to generate one"
+  -- Materialize all dependencies
+  let ws := ws.addPackage ws.root
+  ws.resolveDepsCore fun pkg dep => do
+    let ws ← getWorkspace
+    if let some entry := pkgEntries.find? dep.name then
+      let result ← entry.materialize ws.lakeEnv ws.dir relPkgsDir
+      loadDepPackage result dep.opts leanOpts reconfigure
+    else
+      if pkg.name = ws.root.name then
+        error <|
+          s!"dependency '{dep.name}' not in manifest; \
+          use `lake update {dep.name}` to add it"
+      else
+        error <|
+          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)"

backend/core/leanprover--lean4---v4.22.0/src/lean/lake/Lake/Load/Toml.lean

@@ -0,0 +1,450 @@
+/-
+Copyright (c) 2024 Mac Malone. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Mac Malone
+-/
+prelude
+import Lake.Toml.Load
+import Lake.Toml.Decode
+import Lake.Config.Package
+import Lake.Util.Log
+
+open Lean Parser
+open System (FilePath)
+
+/-! # TOML Loader
+
+This module contains the main definitions to load a package from a
+Lake configuration file written in TOML.
+-/
+
+namespace Lake
+
+open Toml
+
+/-! ## General Helpers -/
+
+@[specialize] def decodeFieldCore
+  (name : Name) (decode : Toml.Value → EDecodeM α) [field : ConfigField σ name α]
+  (_ : Table) (val : Value) (cfg : σ)
+: DecodeM σ := fun es =>
+  match decode val es with
+  | .ok a es => .ok (field.set a cfg) es
+  | .error _ es => .ok cfg es
+
+class DecodeField (σ : Type) (name : Name) where
+  decodeField (t : Table) (val : Value) (cfg : σ) : DecodeM σ
+
+export DecodeField (decodeField)
+
+instance [DecodeToml α] [ConfigField σ name α] : DecodeField σ name where
+  decodeField := decodeFieldCore name decodeToml
+
+structure TomlFieldInfo (σ : Type) where
+  decodeAndSet : Table → Value → σ → DecodeM σ
+
+abbrev TomlFieldInfos (σ : Type) :=
+  NameMap (TomlFieldInfo σ)
+
+def TomlFieldInfos.empty : TomlFieldInfos σ := {}
+
+@[inline] def TomlFieldInfos.insert
+  (name : Name) [DecodeField σ name] (infos : TomlFieldInfos σ)
+: TomlFieldInfos σ :=
+  NameMap.insert infos name ⟨decodeField name⟩
+
+class ConfigTomlInfo (α : Type) where
+  fieldInfos : TomlFieldInfos α
+
+def Toml.Table.decodeConfig
+  [EmptyCollection α] [ConfigTomlInfo α] (t : Table)
+: Toml.DecodeM α :=
+  t.foldM (init := {}) fun cfg key val => do
+    if let some info := ConfigTomlInfo.fieldInfos.find? key then
+      info.decodeAndSet t val cfg
+    else
+      return cfg
+
+@[inline] def decodeTableValue (decode : Table → DecodeM α) (v : Value) : EDecodeM α := do
+  ensureDecode <| decode (← v.decodeTable)
+
+/-! ## Value 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) : EDecodeM Glob := do
+  match inline <| Glob.ofString? (← v.decodeString) with
+  | some v => return v
+  | none => throwDecodeErrorAt v.ref "expected glob"
+
+instance : DecodeToml Glob := ⟨Glob.decodeToml⟩
+instance : DecodeToml (Array Glob) := ⟨Value.decodeArrayOrSingleton⟩
+
+protected def LeanOptionValue.decodeToml : Value → EDecodeM LeanOptionValue
+| .string _ v => return .ofString v
+| .boolean _ v => return .ofBool v
+| .integer _ (.ofNat v) => return .ofNat v
+| x => throwDecodeErrorAt x.ref "expected string, boolean, or nonnegative integer"
+
+instance : DecodeToml LeanOptionValue := ⟨LeanOptionValue.decodeToml⟩
+
+protected def LeanOption.decodeToml (v : Value) : EDecodeM 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
+      throwDecodeErrorAt 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 =>
+    throwDecodeErrorAt v.ref "expected array or table"
+
+instance : DecodeToml LeanOption := ⟨LeanOption.decodeToml⟩
+
+protected def BuildType.decodeToml (v : Value) : EDecodeM BuildType := do
+  match inline <| BuildType.ofString? (← v.decodeString) with
+  | some v => return v
+  | none => throwDecodeErrorAt v.ref "expected one of 'debug', 'relWithDebInfo', 'minSizeRel', 'release'"
+
+instance : DecodeToml BuildType := ⟨(BuildType.decodeToml ·)⟩
+
+protected def Backend.decodeToml (v : Value) : EDecodeM Backend := do
+  match inline <| Backend.ofString? (← v.decodeString) with
+  | some v => return v
+  | none => throwDecodeErrorAt v.ref "expected one of 'c', 'llvm', or 'default'"
+
+instance : DecodeToml Backend := ⟨Backend.decodeToml⟩
+
+partial def decodeLeanOptionsAux
+  (v : Value) (k : Name) (vs : EDecodeM (Array LeanOption))
+: EDecodeM (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) : EDecodeM (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 => throwDecodeErrorAt v.ref "expected array or table"
+
+instance : DecodeToml (Array LeanOption) := ⟨decodeLeanOptions⟩
+
+protected def StdVer.decodeToml (v : Value) : EDecodeM LeanVer := do
+  match StdVer.parse (← v.decodeString) with
+  | .ok v => return v
+  | .error e => throwDecodeErrorAt v.ref e
+
+instance : DecodeToml StdVer := ⟨StdVer.decodeToml⟩
+
+mutual
+
+partial def Pattern.decodeToml
+  [IsPattern β α] [DecodeToml β] (v : Value) (presets : NameMap (Pattern α β) := {})
+: EDecodeM (Pattern α β) :=
+  have : DecodeToml (PatternDescr α β) := ⟨PatternDescr.decodeToml⟩
+  match v with
+  | .string _ s =>
+    if s == "*" then
+      return .star
+    else
+      .ofDescr <$> decodeToml v
+  | .table r t => do
+    if let some name ← t.decode? `preset then
+      if let some preset := presets.find? name then
+        return preset
+      else
+        throwDecodeErrorAt r s!"unknown preset '{name}'"
+    else
+      .ofDescr <$> decodeToml v
+  | v => .ofDescr <$> decodeToml v
+
+partial def PatternDescr.decodeToml
+  [IsPattern β α] [DecodeToml β] (v : Value)
+: EDecodeM (PatternDescr α β) :=
+  have : DecodeToml (Pattern α β) := ⟨Pattern.decodeToml⟩
+  match v with
+  | .table _ t => do
+    if let some p ← t.decode? `not then
+      return .not p
+    if let some p ← t.decode? `any then
+      return .any p
+    else if let some p ← t.decode? `all then
+      return .all p
+    else
+      .coe <$> decodeToml v
+  | v => .coe <$> decodeToml v
+
+end
+
+instance [IsPattern β α] [DecodeToml β] : DecodeToml (Pattern α β) := ⟨Pattern.decodeToml⟩
+instance [IsPattern β α] [DecodeToml β] : DecodeToml (PatternDescr α β) := ⟨PatternDescr.decodeToml⟩
+
+protected def StrPatDescr.decodeToml (v : Value) : EDecodeM StrPatDescr :=
+  match v with
+  | .array _ vs => .mem <$> decodeArray vs
+  | .table r t => do
+    if let some affix ← t.decode? `startsWith then
+      return .startsWith affix
+    else if let some affix ← t.decode? `endsWith then
+      return .endsWith affix
+    else
+      throwDecodeErrorAt r "expected string pattern"
+  | v => throwDecodeErrorAt v.ref "expected string pattern"
+
+instance : DecodeToml StrPatDescr := ⟨StrPatDescr.decodeToml⟩
+
+protected def PathPatDescr.decodeToml (v : Value) : EDecodeM PathPatDescr :=
+  match v with
+  | .table r t => do
+    if let some p ← t.decode? `path then
+      return .path p
+    else if let some p ← t.decode? `extension then
+      return .extension p
+    else if let some p ← t.decode? `fileName then
+      return .fileName p
+    else
+      throwDecodeErrorAt r "expected file path pattern"
+  | v => throwDecodeErrorAt v.ref "expected file path pattern"
+
+instance : DecodeToml PathPatDescr := ⟨PathPatDescr.decodeToml⟩
+
+def decodeVersionTags (v : Value) : EDecodeM StrPat :=
+  inline <| Pattern.decodeToml (presets := versionTagPresets) v
+
+instance : DecodeField (PackageConfig n) `versionTags where
+  decodeField := decodeFieldCore `versionTags decodeVersionTags
+
+-- for `platformIndependent`, `releaseRepo`, `buildArchive`, etc.
+instance [DecodeToml α] : DecodeToml (Option α) := ⟨(some <$> decodeToml ·)⟩
+
+def PartialBuildKey.decodeToml (v : Value) : EDecodeM PartialBuildKey := do
+  match PartialBuildKey.parse (← v.decodeString) with
+  | .ok k => return k
+  | .error e => throwDecodeErrorAt v.ref e
+
+instance : DecodeToml PartialBuildKey := ⟨PartialBuildKey.decodeToml⟩
+instance : DecodeToml (Target α) := ⟨(Target.mk <$> PartialBuildKey.decodeToml ·)⟩
+
+def decodeFacets (kind : Name) (val : Value) : EDecodeM (Array Name) := do
+  return (← val.decodeArray).map (kind ++ ·)
+
+instance : DecodeField (LeanLibConfig n) `defaultFacets where
+  decodeField := decodeFieldCore `defaultFacets (decodeFacets LeanLib.facetKind)
+
+-- HACK to work around the fact the TOML decoders
+-- do not support inter-field dependencies by default
+def decodeRoots
+  (t : Table) (v : Value) (cfg : LeanLibConfig n)
+: DecodeM (LeanLibConfig n) := do
+  let cfg ← decodeField `roots t v cfg
+  if t.contains `globs then
+    return cfg
+  else
+    return {cfg with globs := mkFieldDefault `globs cfg}
+
+instance : DecodeField (LeanLibConfig n) `roots := ⟨decodeRoots⟩
+
+/-! ## Dependency Configuration Decoders -/
+
+protected def DependencySrc.decodeToml (t : Table) (ref := Syntax.missing) : EDecodeM DependencySrc := do
+  let typeVal ← t.decodeValue `type
+  match (← typeVal.decodeString) with
+  | "path" =>
+    return .path (← t.decode `dir)
+  | "git" => ensureDecode do
+    return .git (← t.tryDecode `url ref) (← t.tryDecode? `rev) (← t.tryDecode? `subDir)
+  | _ =>
+    throwDecodeErrorAt typeVal.ref "expected one of 'path' or 'git'"
+
+instance : DecodeToml DependencySrc := ⟨fun v => do DependencySrc.decodeToml (← v.decodeTable) v.ref⟩
+
+protected def Dependency.decodeToml (t : Table) (ref := Syntax.missing) : EDecodeM Dependency := ensureDecode do
+  let name ← stringToLegalOrSimpleName <$> t.tryDecode `name ref
+  let rev? ← t.tryDecode? `rev
+  let src? : Option DependencySrc ← id do
+    if let some dir ← t.tryDecode? `path then
+      return some <| .path dir
+    else if let some g := t.find? `git then
+      match g with
+      | .string _ url =>
+        return some <| .git url rev? (← t.tryDecode? `subDir)
+      | .table ref t =>
+        return some <| .git (← t.tryDecode `url ref) rev? (← t.tryDecode? `subDir)
+      | _ =>
+        modify (·.push <| .mk g.ref "expected string or table")
+        return default
+    else
+      t.tryDecode? `source
+  let scope ← t.tryDecodeD `scope ""
+  let version? ← id do
+    if let some ver ← t.tryDecode? `version then
+      return some ver
+    else if let some rev := rev? then
+      return if src?.isSome then none else some s!"git#{rev}"
+    else
+      return none
+  let opts ← t.tryDecodeD `options {}
+  return {name, scope, version?, src?, opts}
+
+instance : DecodeToml Dependency := ⟨fun v => do Dependency.decodeToml (← v.decodeTable) v.ref⟩
+
+/-! ## Package & Target Configuration Decoders -/
+
+private def genDecodeToml
+  (cmds : Array Command)
+  (tyName : Name) [info : ConfigInfo tyName]  (takesName : Bool)
+  (exclude : Array Name := {})
+: MacroM (Array Command) := do
+  let init ← `(TomlFieldInfos.empty)
+  let ty := if takesName then Syntax.mkCApp tyName #[mkIdent `n] else mkCIdent tyName
+  let infos ← info.fields.foldlM (init := init) fun infos {name, parent, ..} =>
+    if parent || exclude.contains name then
+      return infos
+    else
+      `($infos |>.insert $(quote name))
+  let instId ← mkIdentFromRef <| `_root_ ++ tyName.str "instConfigTomlInfo"
+  let cmds ← cmds.push <$> `(instance $instId:ident : ConfigTomlInfo $ty := ⟨$infos⟩)
+  let decId ← mkIdentFromRef <| `_root_ ++ tyName.str "decodeToml"
+  let cmds ← cmds.push <$> `(protected def $decId (t : Table) : DecodeM $ty := t.decodeConfig)
+  let instId ← mkIdentFromRef <| `_root_ ++ tyName.str "instDecodeToml"
+  let cmds ← cmds.push <$> `(instance $instId:ident : DecodeToml $ty := ⟨decodeTableValue $decId⟩)
+  return cmds
+
+local macro "gen_toml_decoders%" : command => do
+  let cmds := #[]
+  -- Targets
+  let cmds ← genDecodeToml cmds ``LeanConfig false
+  let cmds ← genDecodeToml cmds ``LeanLibConfig true
+    (exclude := #[`nativeFacets])
+  let cmds ← genDecodeToml cmds ``LeanExeConfig true
+    (exclude := #[`nativeFacets])
+  let cmds ← genDecodeToml cmds ``InputFileConfig true
+  let cmds ← genDecodeToml cmds ``InputDirConfig true
+  -- Package
+  let cmds ← genDecodeToml cmds ``WorkspaceConfig false
+  let cmds ← genDecodeToml cmds ``PackageConfig true
+  return ⟨mkNullNode cmds⟩
+
+gen_toml_decoders%
+
+def decodeTargetDecls
+  (pkg : Name) (t : Table)
+: DecodeM (Array (PConfigDecl pkg) × DNameMap (NConfigDecl pkg)) := do
+  let r := (#[], {})
+  let r ← go r LeanLib.keyword LeanLib.configKind LeanLibConfig.decodeToml
+  let r ← go r LeanExe.keyword LeanExe.configKind LeanExeConfig.decodeToml
+  let r ← go r InputFile.keyword InputFile.configKind InputFileConfig.decodeToml
+  let r ← go r InputDir.keyword InputDir.configKind InputDirConfig.decodeToml
+  return r
+where
+  go r kw kind (decode : {n : Name} → Table → DecodeM (ConfigType kind pkg n)) := do
+    let some tableArrayVal := t.find? kw | return r
+    let some vals ← tryDecode? tableArrayVal.decodeValueArray | return r
+    vals.foldlM (init := r) fun r val => do
+      let some t ← tryDecode? val.decodeTable | return r
+      let some name ← tryDecode? <| stringToLegalOrSimpleName <$> t.decode `name
+        | return r
+      let (decls, map) := r
+      if let some orig := map.find? name then
+        modify fun es => es.push <| .mk val.ref s!"\
+          {pkg}: target '{name}' was already defined as a '{orig.kind}', \
+          but then redefined as a '{kind}'"
+        return (decls, map)
+      else
+        let config ← @decode name t
+        let decl : NConfigDecl pkg name :=
+          -- Safety: By definition, config kind = facet kind for declarative configurations.
+          unsafe {pkg, name, kind, config, wf_data := lcProof}
+        return (decls.push decl.toPConfigDecl, map.insert name decl)
+
+/-! ## Root Loader -/
+
+/-- Load a `Package` from a Lake configuration file written in TOML. -/
+def loadTomlConfig (cfg: LoadConfig) : LogIO Package := do
+  let input ← IO.FS.readFile cfg.configFile
+  let ictx := mkInputContext input cfg.relConfigFile.toString
+  match (← loadToml ictx |>.toBaseIO) with
+  | .ok table =>
+    let .ok pkg errs := EStateM.run (s := #[]) do
+      let name ← stringToLegalOrSimpleName <$> table.tryDecode `name
+      let config ← @PackageConfig.decodeToml name table
+      let (targetDecls, targetDeclMap) ← decodeTargetDecls name table
+      let defaultTargets ← table.tryDecodeD `defaultTargets #[]
+      let defaultTargets := defaultTargets.map stringToLegalOrSimpleName
+      let depConfigs ← table.tryDecodeD `require #[]
+      return {
+        name := name
+        dir := cfg.pkgDir
+        relDir := cfg.relPkgDir
+        configFile := cfg.configFile
+        relConfigFile := cfg.relConfigFile
+        scope := cfg.scope
+        remoteUrl := cfg.remoteUrl
+        config, depConfigs, targetDecls, targetDeclMap
+        defaultTargets
+      }
+    if errs.isEmpty then
+      return pkg
+    else
+      errorWithLog <| errs.forM fun {ref, msg} =>
+        let pos := ictx.fileMap.toPosition <| ref.getPos?.getD 0
+        logError <| mkErrorStringWithPos ictx.fileName pos msg
+  | .error log =>
+    errorWithLog <| log.forM fun msg => do logError (← msg.toString)

backend/core/leanprover--lean4---v4.22.0/src/lean/lake/Lake/Load/Workspace.lean

@@ -0,0 +1,58 @@
+/-
+Copyright (c) 2024 Mac Malone. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Mac Malone
+-/
+prelude
+import Lake.Load.Resolve
+import Lake.Build.InitFacets
+
+/-! # Workspace Loader
+
+This module contains the main definitions for loading a complete Lake workspace.
+-/
+
+open Lean
+
+namespace Lake
+
+/--
+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.lakeEnv.leanSearchPath
+  let (root, env?) ← loadPackageCore "[root]" config
+  let root ← root.loadInputsFrom config.lakeEnv
+  let ws : Workspace := {
+    root
+    lakeEnv := config.lakeEnv
+    lakeArgs? := config.lakeArgs?
+    facetConfigs := initFacetConfigs
+  }
+  if let some env := env? then
+    IO.ofExcept <| ws.addFacetsFromEnv env config.leanOpts
+  else
+    return ws
+
+/--
+Load a `Workspace` for a Lake package by
+elaborating its configuration file and resolving its dependencies.
+If `updateDeps` is true, updates the manifest before resolving dependencies.
+-/
+def loadWorkspace (config : LoadConfig) : LoggerIO Workspace := do
+  let {reconfigure, leanOpts, updateDeps, updateToolchain, packageOverrides, ..} := config
+  let ws ← loadWorkspaceRoot config
+  if updateDeps then
+    ws.updateAndMaterialize {} leanOpts updateToolchain
+  else if let some manifest ← Manifest.load? ws.manifestFile then
+    ws.materializeDeps manifest leanOpts reconfigure packageOverrides
+  else
+    ws.updateAndMaterialize {} leanOpts updateToolchain
+
+/-- Updates the manifest for the loaded Lake workspace (see `updateAndMaterialize`). -/
+def updateManifest (config : LoadConfig) (toUpdate : NameSet := {})
+: LoggerIO Unit := do
+  let {leanOpts, updateToolchain, ..} := config
+  let ws ← loadWorkspaceRoot config
+  discard <| ws.updateAndMaterialize toUpdate leanOpts updateToolchain

backend/core/leanprover--lean4---v4.22.0/src/lean/lake/Lake/Toml/Data.lean

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

backend/core/leanprover--lean4---v4.22.0/src/lean/lake/Lake/Toml/Decode.lean

@@ -0,0 +1,208 @@
+/-
+Copyright (c) 2024 Mac Malone. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Mac Malone
+-/
+prelude
+import Init.System.FilePath
+import Lake.Toml.Data
+
+open Lean
+
+/-!
+# TOML Decoders
+
+This module contains definitions to assist in decoding TOML data values
+into concrete user types.
+-/
+
+namespace Lake
+
+structure Toml.DecodeError where
+  ref : Syntax
+  msg : String
+
+abbrev Toml.DecodeM := EStateM Empty (Array DecodeError)
+
+abbrev Toml.EDecodeM := EStateM Unit (Array DecodeError)
+
+class DecodeToml (α : Type) where
+  decode (v : Toml.Value) : Toml.EDecodeM α
+
+abbrev decodeToml [DecodeToml α] (v : Toml.Value) : Toml.EDecodeM α :=
+  DecodeToml.decode v
+
+namespace Toml
+
+/-- Run the decode action. If there were errors, throw. Otherwise, return the result. -/
+@[inline] def ensureDecode (x : DecodeM α) : EDecodeM α := fun es =>
+  match x es with
+  | .ok a es => if es.isEmpty then .ok a es else .error () es
+
+/-- Run the decode action. If it fails, keep the errors but return `default`. -/
+@[inline] def tryDecodeD (default : α) (x : EDecodeM α) : DecodeM α := fun es =>
+  match x es with
+  | .ok a es => .ok a es
+  | .error _ es => .ok default es
+
+/-- Run the decode action. If it fails, keep the errors but  return `none`. -/
+@[inline] def tryDecode? (x : EDecodeM α) : DecodeM (Option α) := fun es =>
+   match x es with
+  | .ok a es => .ok (some a) es
+  | .error _ es => .ok none es
+
+/-- Run the decode action. If it fails, keep the errors but  return `Inhabited.default`. -/
+@[inline] def tryDecode [Inhabited α] (x : EDecodeM α) : DecodeM α :=
+  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 : α → EDecodeM β) : DecodeM β :=
+  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 : α → EDecodeM β) : DecodeM β :=
+  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 result in `some`.
+-/
+@[inline] def optDecode? (a? : Option α)  (f : α → EDecodeM β) : DecodeM (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₁ : EDecodeM α) (x₂ : EDecodeM β) (f : α → β → γ) : EDecodeM γ := fun es =>
+  match x₁ es with
+  | .ok a es =>
+    match x₂ es with
+    | .ok b es => .ok (f a b) es
+    | .error _ es => .error () es
+  | .error _ es => .error () es
+
+@[inline] def throwDecodeErrorAt (ref : Syntax) (msg : String) : EDecodeM α :=
+  fun es => .error () (es.push {ref, msg})
+
+/-- Decode an array of TOML values, merging any errors from the elements into a single array. -/
+def decodeArray [dec : DecodeToml α] (vs : Array Value) : EDecodeM (Array α) :=
+  vs.foldl (init := pure (.mkEmpty vs.size)) fun vs v =>
+    mergeErrors vs (dec.decode v) Array.push
+
+instance : DecodeToml Value := ⟨pure⟩
+
+namespace Value
+
+def decodeString : Value → EDecodeM String
+| .string _ v => .ok v
+| x => throwDecodeErrorAt x.ref "expected string"
+
+instance : DecodeToml String := ⟨decodeString⟩
+instance : DecodeToml System.FilePath := ⟨(.mk <$> decodeToml ·)⟩
+
+def decodeName (v : Value) : EDecodeM Name := do
+  match (← v.decodeString).toName with
+  | .anonymous => throwDecodeErrorAt v.ref "expected name"
+  | n => pure n
+
+instance : DecodeToml Lean.Name := ⟨decodeName⟩
+
+def decodeInt : Value → EDecodeM Int
+| .integer _ v => .ok v
+| x => throwDecodeErrorAt x.ref "expected integer"
+
+instance : DecodeToml Int := ⟨decodeInt⟩
+
+def decodeNat : Value → EDecodeM Nat
+| .integer _ (.ofNat v) => .ok v
+| x => throwDecodeErrorAt x.ref "expected nonnegative integer"
+
+instance : DecodeToml Nat := ⟨decodeNat⟩
+
+def decodeFloat : Value → EDecodeM Float
+| .float _ v => .ok v
+| x => throwDecodeErrorAt x.ref "expected float"
+
+instance : DecodeToml Float := ⟨decodeFloat⟩
+
+def decodeBool : Value → EDecodeM Bool
+| .boolean _ v => .ok v
+| x => throwDecodeErrorAt x.ref "expected boolean"
+
+instance : DecodeToml Bool := ⟨decodeBool⟩
+
+def decodeDateTime : Value → EDecodeM DateTime
+| .dateTime _ v => .ok v
+| x => throwDecodeErrorAt x.ref "expected date-time"
+
+instance : DecodeToml DateTime := ⟨decodeDateTime⟩
+
+def decodeValueArray : Value → EDecodeM (Array Value)
+| .array _ vs => .ok vs
+| x => throwDecodeErrorAt x.ref "expected array"
+
+@[inline] protected def decodeArray [dec : DecodeToml α] (v : Value) : EDecodeM (Array α) := do
+  decodeArray (dec := dec) (← v.decodeValueArray)
+
+instance [DecodeToml α] : DecodeToml (Array α) := ⟨Value.decodeArray⟩
+
+@[inline] def decodeArrayOrSingleton [dec : DecodeToml α] : Value → EDecodeM (Array α)
+| .array _ vs => decodeArray (dec := dec) vs
+| v => Array.singleton <$> dec.decode v
+
+def decodeTable : Value → EDecodeM Table
+| .table _ t => .ok t
+| x => throwDecodeErrorAt x.ref "expected table"
+
+instance : DecodeToml Table := ⟨(·.decodeTable)⟩
+
+end Value
+
+def decodeKeyval [dec : DecodeToml α] (k : Name) (v : Value) : EDecodeM α := fun es =>
+  let iniPos := es.size
+  let f es := es.mapIdx fun i e =>
+    if iniPos ≤ i then {e with msg := s!"key {ppKey k}: {e.msg}"} else e
+  match dec.decode v es with
+  | .ok a es => .ok a (f es)
+  | .error e es => .error e (f es)
+
+namespace Table
+
+def decodeValue (t : Table) (k : Name) (ref := Syntax.missing) : EDecodeM Value := do
+  let some a := t.find? k
+    | throwDecodeErrorAt ref s!"missing required key: {ppKey k}"
+  return a
+
+@[inline] def decode [dec : DecodeToml α] (t : Table) (k : Name) (ref := Syntax.missing) : EDecodeM α := do
+  let a ← t.decodeValue k ref
+  decodeKeyval (dec := dec) k a
+
+@[inline] def decode? [dec : DecodeToml α] (t : Table) (k : Name) : EDecodeM (Option α) := do
+  t.find? k |>.mapM fun v => decodeKeyval (dec := dec) k v
+
+def decodeNameMap [dec : DecodeToml α] (t : Toml.Table) : EDecodeM (NameMap α) := do
+  t.items.foldl (init := pure {}) 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) : DecodeM α := do
+  tryDecode <| t.decode (dec := dec) k ref
+
+@[inline] protected def tryDecode? [dec : DecodeToml α] (t : Table) (k : Name) : DecodeM (Option α) :=
+  optDecode? (t.find? k) dec.decode
+
+@[inline] protected def tryDecodeD [dec : DecodeToml α] (k : Name) (default : α) (t : Table) : DecodeM α :=
+  optDecodeD default (t.find? k) dec.decode
+
+end Table