feat: lake: fixedToolchain package configuration (#12935)

This PR adds the `fixedToolchain` Lake package configuration option.
Setting this to `true` informs Lake that the package is only expected to
function on a single toolchain (like Mathlib). This causes Lake's
toolchain update procedure to prioritize its toolchain and avoids the
need to separate input-to-output mappings for the package by toolchain
version in the Lake cache.

src/lake/Lake/CLI/Main.lean

@@ -392,7 +392,7 @@ def serviceNotFound (service : String) (configuredServices : Array CacheServiceC
     configuredServices.foldl (· ++ s!"  {·.name}") msg
 
 @[inline] private def cacheToolchain (pkg : Package) (toolchain : CacheToolchain) : CacheToolchain :=
-  if pkg.bootstrap then .none else toolchain
+  if pkg.fixedToolchain || pkg.bootstrap then .none else toolchain
 
 @[inline] private def cachePlatform (pkg : Package) (platform : CachePlatform) : CachePlatform :=
   if pkg.isPlatformIndependent then .none else platform

src/lake/Lake/Config/Package.lean

@@ -45,7 +45,7 @@ public structure Package where
   /-- The path to the package's configuration file (relative to `dir`). -/
   relConfigFile : FilePath
   /-- The path to the package's JSON manifest of remote dependencies (relative to `dir`). -/
-  relManifestFile : FilePath := config.manifestFile.getD defaultManifestFile |>.normalize
+  relManifestFile : FilePath := defaultManifestFile
   /-- The package's scope (e.g., in Reservoir). -/
   scope : String
   /-- The URL to this package's Git remote. -/
@@ -244,6 +244,10 @@ public def id? (self : Package) : Option PkgId :=
 @[inline] public def isPlatformIndependent (self : Package) : Bool :=
   self.config.platformIndependent == some true
 
+/-- The package's `fixedToolchain` configuration. -/
+@[inline] public def fixedToolchain (self : Package) : Bool :=
+  self.config.fixedToolchain
+
 /-- The package's `releaseRepo`/`releaseRepo?` configuration. -/
 @[inline] public def releaseRepo? (self : Package) : Option String :=
   self.config.releaseRepo

src/lake/Lake/Config/PackageConfig.lean

@@ -29,16 +29,6 @@ public configuration PackageConfig (p : Name) (n : Name) extends WorkspaceConfig
   /-- **For internal use.** Whether this package is Lean itself. -/
   bootstrap : Bool := false
 
-  /--
-  **This field is deprecated.**
-
-  The path of a package's manifest file, which stores the exact versions
-  of its resolved dependencies.
-
-  Defaults to `defaultManifestFile` (i.e., `lake-manifest.json`).
-  -/
-  manifestFile : Option FilePath := none
-
   /-- An `Array` of target names to build whenever the package is used. -/
   extraDepTargets : Array Name := #[]
 
@@ -331,6 +321,18 @@ public configuration PackageConfig (p : Name) (n : Name) extends WorkspaceConfig
   -/
   allowImportAll : Bool := false
 
+  /--
+  Whether this package is expected to function only on a single toolchain
+  (the package's toolchain).
+
+  This informs Lake's toolchain update procedure (in `lake update`) to prioritize
+  this package's toolchain. It also avoids the need to separate input-to-output mappings
+  for this package by toolchain version in the Lake cache.
+
+  Defaults to `false`.
+  -/
+  fixedToolchain : Bool := false
+
 deriving Inhabited
 
 /-- The package's name as specified by the author. -/

src/lake/Lake/Load/Lean/Eval.lean

@@ -166,10 +166,6 @@ public def Package.loadFromEnv
     else
       pure self.config.lintDriver
 
-  -- Deprecation warnings
-  unless self.config.manifestFile.isNone do
-    logWarning s!"{self.prettyName}: package configuration option 'manifestFile' is deprecated"
-
   -- Fill in the Package
   return {self with
     depConfigs, targetDecls, targetDeclMap

src/lake/Lake/Load/Manifest.lean

@@ -50,8 +50,9 @@ That is, Lake ignores the `-` suffix.
 **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
+- `"1.2.0"`: Add optional `fixedToolchain` manifest field
 -/
-@[inline] public def Manifest.version : StdVer := {major := 1, minor := 1}
+@[inline] public def Manifest.version : StdVer := {major := 1, minor := 2}
 
 /-- Manifest version `0.6.0` package entry. For backwards compatibility. -/
 private inductive PackageEntryV6
@@ -84,7 +85,9 @@ public structure PackageEntry where
   name : Name
   scope : String := ""
   inherited : Bool
+  /-- The relative path within the package directory to the Lake configuration file. -/
   configFile : FilePath := defaultConfigFile
+  /-- The relative path within the package directory to the Lake manifest file. -/
   manifestFile? : Option FilePath := none
   src : PackageEntrySrc
   deriving Inhabited
@@ -139,7 +142,7 @@ public protected def fromJson? (json : Json) : Except String PackageEntry := do
       | _ =>
         throw s!"unknown package entry type '{type}'"
     return {
-      name, scope, inherited,
+      name, scope, inherited
       configFile, manifestFile? := manifestFile, src
       : PackageEntry
     }
@@ -172,6 +175,7 @@ end PackageEntry
 public structure Manifest where
   name : Name
   lakeDir : FilePath
+  fixedToolchain : Bool
   packagesDir? : Option FilePath := none
   packages : Array PackageEntry := #[]
 
@@ -184,6 +188,7 @@ public def addPackage (entry : PackageEntry) (self : Manifest) : Manifest :=
 public protected def toJson (self : Manifest) : Json :=
   Json.mkObj [
     ("version", toJson version),
+    ("fixedToolchain", toJson self.fixedToolchain),
     ("name", toJson self.name),
     ("lakeDir", toJson self.lakeDir),
     ("packagesDir", toJson self.packagesDir?),
@@ -217,11 +222,12 @@ private def getPackages (ver : StdVer) (obj : JsonObject) : Except String (Array
 public protected def fromJson? (json : Json) : Except String Manifest := do
   let obj ← JsonObject.fromJson? json
   let ver ← getVersion obj
+  let fixedToolchain ← obj.getD "fixedToolchain" false
   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}
+  return {name, lakeDir, packagesDir?, packages, fixedToolchain}
 
 public instance : FromJson Manifest := ⟨Manifest.fromJson?⟩
 

src/lake/Lake/Load/Materialize.lean

@@ -89,26 +89,33 @@ public structure MaterializedDep where
   Used as the endpoint from which to fetch cloud releases for the package.
   -/
   remoteUrl : String
+  /-- The manifest for the dependency or the error produced when trying to load it. -/
+  manifest? : Except IO.Error Manifest
   /-- The manifest entry for the dependency. -/
   manifestEntry : PackageEntry
   deriving Inhabited
 
 namespace MaterializedDep
 
-@[inline] public def name (self : MaterializedDep) :=
+@[inline] public def name (self : MaterializedDep) : Name :=
   self.manifestEntry.name
 
-@[inline] public def scope (self : MaterializedDep) :=
+@[inline] public def scope (self : MaterializedDep) : String :=
   self.manifestEntry.scope
 
 /-- Path to the dependency's configuration file (relative to `relPkgDir`). -/
-@[inline] public def manifestFile? (self : MaterializedDep) :=
+@[inline] public def manifestFile? (self : MaterializedDep) : Option FilePath :=
   self.manifestEntry.manifestFile?
 
 /-- Path to the dependency's configuration file (relative to `relPkgDir`). -/
-@[inline] public def configFile (self : MaterializedDep) :=
+@[inline] public def configFile (self : MaterializedDep) : FilePath :=
   self.manifestEntry.configFile
 
+public def fixedToolchain (self : MaterializedDep) : Bool :=
+  match self.manifest? with
+  | .ok manifest => manifest.fixedToolchain
+  | _ => false
+
 end MaterializedDep
 
 inductive InputVer
@@ -148,7 +155,7 @@ public def Dependency.materialize
     match src with
     | .path dir =>
       let relPkgDir := relParentDir / dir
-      return mkDep relPkgDir "" (.path relPkgDir)
+      mkDep (wsDir / relPkgDir) relPkgDir "" (.path relPkgDir)
     | .git url inputRev? subDir? => do
       let sname := dep.name.toString (escape := false)
       let repoUrl := Git.filterUrl? url |>.getD ""
@@ -196,16 +203,19 @@ public def Dependency.materialize
     | _ => error s!"{pkg.fullName}: Git source not found on Reservoir"
 where
   materializeGit name relPkgDir gitUrl remoteUrl inputRev? subDir? : LoggerIO MaterializedDep := do
-    let repo := GitRepo.mk (wsDir / relPkgDir)
+    let pkgDir := wsDir / relPkgDir
+    let repo := GitRepo.mk pkgDir
     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}
-  }
+    mkDep pkgDir relPkgDir remoteUrl <| .git gitUrl rev inputRev? subDir?
+  @[inline] mkDep pkgDir relPkgDir remoteUrl src : LoggerIO MaterializedDep := do
+    return {
+      relPkgDir, remoteUrl
+      manifest? :=  ← Manifest.load (pkgDir / defaultManifestFile) |>.toBaseIO
+      manifestEntry := {name := dep.name, scope := dep.scope, inherited, src}
+    }
 
 /--
 Materializes a manifest package entry, cloning and/or checking it out as necessary.
@@ -216,7 +226,7 @@ public def PackageEntry.materialize
 : LoggerIO MaterializedDep :=
   match manifestEntry.src with
   | .path (dir := relPkgDir) .. =>
-    return mkDep relPkgDir ""
+    mkDep (wsDir / relPkgDir) relPkgDir ""
   | .git (url := url) (rev := rev) (subDir? := subDir?) .. => do
     let sname := manifestEntry.name.toString (escape := false)
     let relGitDir := relPkgsDir / sname
@@ -239,7 +249,12 @@ public def PackageEntry.materialize
       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 "")
+    mkDep gitDir relPkgDir (Git.filterUrl? url |>.getD "")
 where
-  @[inline] mkDep relPkgDir remoteUrl : MaterializedDep :=
-    {relPkgDir, remoteUrl, manifestEntry}
+  @[inline] mkDep pkgDir relPkgDir remoteUrl : LoggerIO MaterializedDep := do
+    let manifest? ← id do
+      if let some manifestFile := manifestEntry.manifestFile? then
+        Manifest.load (pkgDir / manifestFile) |>.toBaseIO
+      else
+        return .error (.noFileOrDirectory "" 0 "")
+    return {relPkgDir, remoteUrl, manifest?, manifestEntry}

src/lake/Lake/Load/Resolve.lean

@@ -171,8 +171,8 @@ private def reuseManifest
     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
+private def addDependencyEntries (pkg : Package) (matDep : MaterializedDep) : UpdateT LoggerIO PUnit := do
+  match matDep.manifest? with
   | .ok manifest =>
     manifest.packages.forM fun entry => do
       unless (← getThe (NameMap PackageEntry)).contains entry.name do
@@ -210,6 +210,36 @@ Used, for instance, if the toolchain is updated and no Elan is detected.
 -/
 def restartCode : ExitCode := 4
 
+/-- The toolchain information of a package. -/
+private structure ToolchainCandidate where
+  /-- The name of the package which provided the toolchain candidate. -/
+  src : Name
+  /-- The version of the toolchain candidate. -/
+  ver : ToolchainVer
+  /-- Whether the candidate toolchain been fixed to particular version. -/
+  fixed : Bool := false
+
+private structure ToolchainState where
+  /-- The name of depedency which provided the current candidate toolchain. -/
+  src : Name
+  /-- The current candidate toolchain version (if any). -/
+  tc? : Option ToolchainVer
+  /-- Incompatible candidate toolchains (if any). -/
+  clashes : Array ToolchainCandidate
+  /--
+  Whether the candidate toolchain been fixed to particular version.
+  If `false`, the search will update the toolchain further where possible.
+  -/
+  fixed : Bool
+
+@[inline] def ToolchainState.replace
+  (src : Name) (tc? : Option ToolchainVer) (fixed : Bool) (self : ToolchainState)
+: ToolchainState := {self with src, tc?, fixed}
+
+@[inline] def ToolchainState.addClash
+  (src : Name) (ver : ToolchainVer) (fixed : Bool) (self : ToolchainState)
+: ToolchainState := {self with clashes := self.clashes.push {src, ver, fixed}}
+
 /--
 Update the workspace's `lean-toolchain` if necessary.
 
@@ -222,23 +252,38 @@ def Workspace.updateToolchain
 : LoggerIO PUnit := do
   let rootToolchainFile := ws.root.dir / toolchainFileName
   let rootTc? ← ToolchainVer.ofDir? ws.dir
-  let (src, tc?, tcs) ← rootDeps.foldlM (init := (ws.root.baseName, rootTc?, #[])) fun s dep => do
+  let s : ToolchainState := ⟨ws.root.baseName, rootTc?, #[], ws.root.fixedToolchain⟩
+  let ⟨src, tc?, tcs, fixed⟩ ← rootDeps.foldlM (init := s) 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)
+    let some tc := s.tc?
+      | return s.replace dep.name depTc? dep.fixedToolchain
+    if dep.fixedToolchain then
+      if s.fixed then
+        if tc = depTc then
+          return s
+        else
+          return s.addClash dep.name depTc dep.fixedToolchain -- true
+      else
+        if tc ≤ depTc then
+          return s.replace dep.name depTc dep.fixedToolchain -- true
+        else
+          return s.addClash dep.name depTc dep.fixedToolchain -- true
     else
-      return (src, tc, tcs.push (dep.name, depTc))
+      if depTc ≤ tc then
+        return s
+      else if !s.fixed && tc < depTc then
+        return s.replace dep.name depTc dep.fixedToolchain -- false
+      else
+        return s.addClash dep.name depTc dep.fixedToolchain -- false
   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}"
+    let addEntry s tc src fixed :=
+      let fixed := if fixed then " (fixed toolchain)" else ""
+      s!"{s}\n  {tc}\n    from {src}{fixed}"
+    let s := if let some tc := tc? then addEntry s tc src fixed else s
+    let s := tcs.foldl (init := s) fun s ⟨src, tc, fixed⟩ => addEntry s tc src fixed
     logWarning s
   else if let some tc := tc? then
     if rootTc?.any (· == tc) then
@@ -333,7 +378,7 @@ where
     loadUpdatedDep wsIdx dep matDep
   @[inline] loadUpdatedDep wsIdx dep matDep : StateT Workspace (UpdateT LoggerIO) Package  := do
     let depPkg ← loadDepPackage wsIdx matDep dep.opts leanOpts true
-    addDependencyEntries depPkg
+    addDependencyEntries depPkg matDep
     return depPkg
 
 /-- Write package entries to the workspace manifest. -/
@@ -347,6 +392,7 @@ def Workspace.writeManifest
     | none => arr -- should only be the case for the root
   let manifest : Manifest := {
     name := ws.root.baseName
+    fixedToolchain := ws.root.fixedToolchain
     lakeDir := ws.relLakeDir
     packagesDir? := ws.relPkgsDir
     packages := manifestEntries

src/lake/schemas/lakefile-toml-schema.json

@@ -462,6 +462,11 @@
                     "default": false,
                     "description": "Whether downstream packages can `import all` modules of this package.\n\nIf enabled, downstream users will be able to access the `private` internals of modules, including definition bodies not marked as `@[expose]`. This may also, in the future, prevent compiler optimization which rely on `private` definitions being inaccessible outside their own package."
                 },
+                "fixedToolchain": {
+                    "type": "boolean",
+                    "default": false,
+                    "description": "Whether this package is expected to only function on a single toolchain (the package's toolchain).\n\nThis informs Lake's toolchain update procedure (in `lake update`) to prioritize this package's toolchain. It also avoids the need to separate input-to-output mappings for this package by toolchain version in the Lake cache."
+                },
                 "enableArtifactCache": {
                     "type": "boolean",
                     "description": "Whether to enables Lake's local, offline artifact cache for the package.\n\nArtifacts (i.e., build products) of packages will be shared across local copies by storing them in a cache associated with the Lean toolchain.\nThis can significantly reduce initial build times and disk space usage when working with multiple copies of large projects or large dependencies.\n\nAs a caveat, build targets which support the artifact cache will not be stored in their usual location within the build directory. Thus, projects with custom build scripts that rely on specific location of artifacts may wish to disable this feature.\n\nIf `none` (the default), this will fallback to (in order):\n* The `LAKE_ARTIFACT_CACHE` environment variable (if set).\n* The workspace root's `enableArtifactCache` configuration (if set and this package is a dependency).\n* **Lake's default**: The package can use artifacts from the cache, but cannot write to it."

tests/lake/examples/deps/bar/lake-manifest.expected.json

@@ -1,4 +1,4 @@
-{"version": "1.1.0",
+{"version": "1.2.0",
  "packagesDir": ".lake/packages",
  "packages":
  [{"type": "path",
@@ -30,4 +30,5 @@
    "dir": "../foo/../b/../root",
    "configFile": "lakefile.lean"}],
  "name": "bar",
- "lakeDir": ".lake"}
+ "lakeDir": ".lake",
+ "fixedToolchain": false}

tests/lake/tests/manifest/lake-manifest-latest.json

@@ -1,4 +1,4 @@
-{"version": "1.1.0",
+{"version": "1.2.0",
  "packagesDir": ".lake/packages",
  "packages":
  [{"url": "bar",
@@ -19,4 +19,5 @@
    "dir": "foo",
    "configFile": "lakefile.lean"}],
  "name": "«foo-bar»",
- "lakeDir": ".lake"}
+ "lakeDir": ".lake",
+ "fixedToolchain": false}

tests/lake/tests/manifest/lake-manifest-v1.2.0.json

@@ -0,0 +1,23 @@
+{"version": "1.2.0",
+ "packagesDir": ".lake/packages",
+ "packages":
+ [{"url": "bar",
+   "type": "git",
+   "subDir": null,
+   "scope": "foo",
+   "rev": "0538596b94a0510f55dc820cabd3bde41ad93c3e",
+   "name": "bar",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": null,
+   "inherited": false,
+   "configFile": "lakefile.lean"},
+  {"type": "path",
+   "scope": "",
+   "name": "foo",
+   "manifestFile": "lake-manifest.json",
+   "inherited": false,
+   "dir": "foo",
+   "configFile": "lakefile.lean"}],
+ "name": "«foo-bar»",
+ "lakeDir": ".lake",
+ "fixedToolchain": false}

tests/lake/tests/manifest/test.sh

@@ -18,7 +18,7 @@ LOCKED_REV='0538596b94a0510f55dc820cabd3bde41ad93c3e'
 test_update() {
   test_run update
   sed_i "s/$GIT_REV/$LOCKED_REV/g" lake-manifest.json
-  diff --strip-trailing-cr lake-manifest-latest.json lake-manifest.json
+  test_cmd diff -u --strip-trailing-cr lake-manifest-latest.json lake-manifest.json
 }
 
 # ---
@@ -53,6 +53,7 @@ test_manifest v6
 test_manifest v7
 test_manifest v1.0.0
 test_manifest v1.1.0
+test_manifest v1.2.0
 
 # cleanup
 rm -rf bar/.git

tests/lake/tests/updateToolchain/a/lakefile.lean

@@ -0,0 +1,8 @@
+import Lake
+open System Lake DSL
+
+def fixedToolchain : Bool :=
+   get_config? fixedToolchain |>.bind envToBool? |>.getD false
+
+package a where
+  fixedToolchain := fixedToolchain

tests/lake/tests/updateToolchain/a/lakefile.toml

@@ -1 +0,0 @@
-name = "a"

tests/lake/tests/updateToolchain/b/lakefile.lean

@@ -0,0 +1,8 @@
+import Lake
+open System Lake DSL
+
+def fixedToolchain : Bool :=
+   get_config? fixedToolchain |>.bind envToBool? |>.getD false
+
+package b where
+  fixedToolchain := fixedToolchain

tests/lake/tests/updateToolchain/b/lakefile.toml

@@ -1 +0,0 @@
-name = "b"

tests/lake/tests/updateToolchain/clean.sh

@@ -1 +1,4 @@
-rm -f produced.out lean-toolchain a/lean-toolchain b/lean-toolchain
+rm -f produced.out
+rm -rf a/.lake b/.lake
+rm -f lean-toolchain a/lean-toolchain b/lean-toolchain
+rm -f lake-manifest.json a/lake-manifest.json b/lake-manifest.json

tests/lake/tests/updateToolchain/test.sh

@@ -1,9 +1,13 @@
 #!/usr/bin/env bash
 source ../common.sh
+./clean.sh
 
-# Ensure Lake thinks there is a elan environment configured
+# Ensure Lake thinks there is a Elan environment configured
 export ELAN_HOME=
 
+# Ensure Lake does not run a system Elan
+export ELAN=false
+
 # Tests the toolchain update functionality of `lake update`
 
 RESTART_CODE=4
@@ -61,6 +65,20 @@ echo lean-a > a/lean-toolchain
 echo lean-b > b/lean-toolchain
 test_out "toolchain not updated; multiple toolchain candidates" update
 
+# Test a fixed toolchain and a greater version
+./clean.sh
+test_run -d a update -R -KfixedToolchain=true
+echo v4.4.0 > a/lean-toolchain
+echo v4.8.0 > b/lean-toolchain
+test_out "(fixed toolchain)" update
+
+# Test a fixed toolchain and a lower version
+./clean.sh
+test_run -d b update -R -KfixedToolchain=true
+echo v4.4.0 > a/lean-toolchain
+echo v4.8.0 > b/lean-toolchain
+test_update leanprover/lean4:v4.8.0
+
 # Test manual restart
 ./clean.sh
 echo lean-a > a/lean-toolchain
@@ -72,4 +90,4 @@ echo lean-a > a/lean-toolchain
 ELAN=echo test_out "run --install lean-a lake update" update
 
 # Cleanup
-rm -f produced.out
+./clean.sh