refactor: lake: more flexible manifest

RELEASES.md

@@ -13,6 +13,8 @@ v4.4.0 (development in progress)
 
 * By default, `simp` will no longer try to use Decidable instances to rewrite terms. In particular, not all decidable goals will be closed by `simp`, and the `decide` tactic may be useful in such cases. The `decide` simp configuration option can be used to locally restore the old `simp` behavior, as in `simp (config := {decide := true})`; this includes using Decidable instances to verify side goals such as numeric inequalities.
 * **Lake:** Moved the default build directory (e.g., `build`), default packages directory (e.g., `lake-packages`), and the compiled configuration (e.g., `lakefile.olean`) into a new dedicated directory for Lake outputs, `.lake`. The cloud release build archives are also stored here, fixing [#2713](https://github.com/leanprover/lean4/issues/2713).
+* **Lake:** Update manifest format to version 7 (see [lean4#2801](https://github.com/leanprover/lean4/pull/2801) for details on the changes).
+* **Lake:** Deprecate the `manifestFile` field of a package configuration.
 
 v4.3.0
 ---------

src/lake/Lake/Config/Package.lean

@@ -12,6 +12,7 @@ import Lake.Config.Dependency
 import Lake.Config.Script
 import Lake.Util.DRBMap
 import Lake.Util.OrdHashSet
+import Lake.Load.Config
 
 open System Lean
 
@@ -51,9 +52,6 @@ def stringToLegalOrSimpleName (s : String) : Name :=
 /-! # Defaults -/
 --------------------------------------------------------------------------------
 
-/-- The default setting for a `PackageConfig`'s `manifestFile` option. -/
-def defaultManifestFile := "lake-manifest.json"
-
 /-- The default setting for a `PackageConfig`'s `buildDir` option. -/
 def defaultBuildDir : FilePath := "build"
 
@@ -80,12 +78,14 @@ structure PackageConfig extends WorkspaceConfig, LeanConfig where
   name : Name
 
   /--
+  **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 := defaultManifestFile
+  manifestFile : Option FilePath := none
 
   /-- An `Array` of target names to build whenever the package is used. -/
   extraDepTargets : Array Name := #[]
@@ -178,12 +178,18 @@ declare_opaque_type OpaquePostUpdateHook (pkg : Name)
 structure Package where
   /-- The path to the package's directory. -/
   dir : FilePath
+  /-- The path to the package's directory relative to the workspace. -/
+  relDir : FilePath
   /-- The package's user-defined configuration. -/
   config : PackageConfig
   /-- The elaboration environment of the package's configuration file. -/
   configEnv : Environment
   /-- The Lean `Options` the package configuration was elaborated with. -/
   leanOpts : Options
+  /-- The path to the package's configuration file. -/
+  configFile : FilePath
+  /-- The path to the package's JSON manifest of remote dependencies (relative to `dir`). -/
+  relManifestFile : FilePath := config.manifestFile.getD defaultManifestFile
   /-- The URL to this package's Git remote. -/
   remoteUrl? : Option String := none
   /-- (Opaque references to) the package's direct dependencies. -/
@@ -280,9 +286,9 @@ namespace Package
 @[inline] def pkgsDir (self : Package) : FilePath :=
   self.dir / self.relPkgsDir
 
-/-- The package's JSON manifest of remote dependencies. -/
+/-- The path to the package's JSON manifest of remote dependencies. -/
 @[inline] def manifestFile (self : Package) : FilePath :=
-  self.dir / self.config.manifestFile
+  self.dir / self.relManifestFile
 
 /-- The package's `dir` joined with its `buildDir` configuration. -/
 @[inline] def buildDir (self : Package) : FilePath :=

src/lake/Lake/Load/Config.lean

@@ -17,6 +17,9 @@ def toolchainFileName : FilePath := "lean-toolchain"
 /-- The default name of the Lake configuration file (i.e., `lakefile.lean`). -/
 def defaultConfigFile : FilePath := "lakefile.lean"
 
+/-- The default name of the Lake manifest file (i.e., `lake-manifest.json`). -/
+def defaultManifestFile := "lake-manifest.json"
+
 /-- Context for loading a Lake configuration. -/
 structure LoadConfig where
   /-- The Lake environment of the load process. -/

src/lake/Lake/Load/Main.lean

@@ -30,14 +30,17 @@ def loadDepsFromEnv (env : Environment) (opts : Options) : Except String (Array
 Elaborate a dependency's configuration file into a `Package`.
 The resulting package does not yet include any dependencies.
 -/
-def MaterializedDep.loadPackage (dep : MaterializedDep) (wsDir : FilePath)
-(leanOpts : Options) (lakeOpts : NameMap String) (reconfigure : Bool) : LogIO Package := do
+def MaterializedDep.loadPackage (dep : MaterializedDep)
+(wsDir : FilePath) (leanOpts : Options) (reconfigure : Bool) : LogIO Package := do
   let dir := wsDir / dep.relPkgDir
   let lakeDir := dir / defaultLakeDir
-  let configEnv ← importConfigFile wsDir dir lakeDir lakeOpts leanOpts (dir / defaultConfigFile) reconfigure
+  let configEnv ← importConfigFile wsDir dir lakeDir dep.configOpts leanOpts (dir / dep.configFile) reconfigure
   let config ← IO.ofExcept <| PackageConfig.loadFromEnv configEnv leanOpts
   return {
-    dir, config, configEnv, leanOpts
+    dir
+    relDir := dep.relPkgDir
+    config, configEnv, leanOpts
+    configFile := dep.configFile
     remoteUrl? := dep.remoteUrl?
   }
 
@@ -52,8 +55,12 @@ def loadWorkspaceRoot (config : LoadConfig) : LogIO Workspace := do
     config.configOpts config.leanOpts config.configFile config.reconfigure
   let pkgConfig ← IO.ofExcept <| PackageConfig.loadFromEnv configEnv config.leanOpts
   let root := {
-    configEnv, leanOpts := config.leanOpts
-    dir := config.rootDir, config := pkgConfig
+    dir := config.rootDir
+    relDir := "."
+    config := pkgConfig
+    configEnv
+    leanOpts := config.leanOpts
+    configFile := config.configFile
   }
   return {
     root, lakeEnv := config.env
@@ -98,49 +105,59 @@ If `reconfigure`, elaborate configuration files while updating, do not use OLean
 -/
 def Workspace.updateAndMaterialize (ws : Workspace)
 (toUpdate : NameSet := {}) (reconfigure := true) : LogIO Workspace := do
-  let res ← StateT.run (s := mkNameMap MaterializedDep) <| EStateT.run' (mkNameMap Package) do
+  let res ← StateT.run (s := mkNameMap MaterializedDep) <|
+    StateT.run' (s := mkNameMap PackageEntry) <| EStateT.run' (mkNameMap Package) do
     -- Use manifest versions of root packages that should not be updated
-    unless toUpdate.isEmpty do
-      for entry in (← Manifest.loadOrEmpty ws.manifestFile) do
-        unless entry.inherited || toUpdate.contains entry.name do
-          let dep ← entry.materialize ws.dir ws.relPkgsDir ws.lakeEnv.pkgUrlMap
-          modifyThe (NameMap MaterializedDep) (·.insert entry.name dep)
-    buildAcyclic (·.1.name) (ws.root, FilePath.mk ".") fun (pkg, relPkgDir) resolve => do
+    if let some manifest ← liftM <| Manifest.load? ws.manifestFile then
+      unless toUpdate.isEmpty do
+        manifest.packages.forM fun entry => do
+          unless entry.inherited || toUpdate.contains entry.name do
+            modifyThe (NameMap PackageEntry) (·.insert entry.name entry)
+      if let some oldRelPkgsDir := manifest.packagesDir? then
+        let oldPkgsDir := ws.dir / oldRelPkgsDir
+        if oldPkgsDir != ws.pkgsDir && (← oldPkgsDir.pathExists) then
+          liftM <| createParentDirs ws.pkgsDir
+          liftM <| IO.FS.rename oldPkgsDir ws.pkgsDir
+    buildAcyclic (·.name) ws.root fun pkg resolve => do
       let inherited := pkg.name != ws.root.name
-      let deps ← IO.ofExcept <| loadDepsFromEnv pkg.configEnv pkg.leanOpts
       -- Materialize this package's dependencies first
+      let deps ← IO.ofExcept <| loadDepsFromEnv pkg.configEnv pkg.leanOpts
       let deps ← deps.mapM fun dep => fetchOrCreate dep.name do
-        dep.materialize inherited ws.dir ws.relPkgsDir relPkgDir ws.lakeEnv.pkgUrlMap
+        if let some entry := (← getThe (NameMap PackageEntry)).find? dep.name then
+          entry.materialize dep ws.dir ws.relPkgsDir ws.lakeEnv.pkgUrlMap
+        else
+          dep.materialize inherited ws.dir ws.relPkgsDir pkg.relDir ws.lakeEnv.pkgUrlMap
       -- Load dependency packages and materialize their locked dependencies
       let deps ← deps.mapM fun dep => do
-        if let .some pkg := (← getThe (NameMap Package)).find? dep.name then
-          return (pkg, dep.relPkgDir)
+        if let some pkg := (← getThe (NameMap Package)).find? dep.name then
+          return pkg
         else
           -- Load the package
-          let depPkg ← dep.loadPackage ws.dir pkg.leanOpts dep.opts reconfigure
+          let depPkg ← dep.loadPackage ws.dir pkg.leanOpts reconfigure
           if depPkg.name ≠ dep.name then
             logWarning s!"{pkg.name}: package '{depPkg.name}' was required as '{dep.name}'"
           -- Materialize locked dependencies
-          for entry in (← Manifest.loadOrEmpty depPkg.manifestFile) do
-            unless (← getThe (NameMap MaterializedDep)).contains entry.name do
-              let entry := entry.setInherited.inDirectory dep.relPkgDir
-              let dep ← entry.materialize ws.dir ws.relPkgsDir ws.lakeEnv.pkgUrlMap
-              modifyThe (NameMap MaterializedDep) (·.insert entry.name dep)
+          if let some manifest ← liftM <| Manifest.load? depPkg.manifestFile then
+            manifest.packages.forM fun entry => do
+              unless (← getThe (NameMap PackageEntry)).contains entry.name do
+                let entry := entry.setInherited.inDirectory dep.relPkgDir
+                modifyThe (NameMap PackageEntry) (·.insert entry.name entry)
           modifyThe (NameMap Package) (·.insert dep.name depPkg)
-          return (depPkg, dep.relPkgDir)
+          return depPkg
       -- Resolve dependencies's dependencies recursively
       return {pkg with opaqueDeps := ← deps.mapM (.mk <$> resolve ·)}
   match res with
   | (.ok root, deps) =>
     let ws : Workspace ← {ws with root}.finalize
     let manifest : Manifest := {
-      name? := ws.root.name
-      lakeDir? := ws.relLakeDir
+      name := ws.root.name
+      lakeDir := ws.relLakeDir
       packagesDir? := ws.relPkgsDir
     }
     let manifest := ws.packages.foldl (init := manifest) fun manifest pkg =>
       match deps.find? pkg.name with
-      | some dep => manifest.addPackage dep.manifestEntry
+      | some dep => manifest.addPackage <|
+        dep.manifestEntry.setManifestFile pkg.relManifestFile
       | none => manifest -- should only be the case for the root
     manifest.saveToFile ws.manifestFile
     LakeT.run ⟨ws⟩ <| ws.packages.forM fun pkg => do
@@ -157,7 +174,7 @@ Resolving a workspace's dependencies using a manifest,
 downloading and/or updating them as necessary.
 -/
 def Workspace.materializeDeps (ws : Workspace) (manifest : Manifest) (reconfigure := false) : LogIO Workspace := do
-  if !manifest.isEmpty && manifest.packagesDir? != some ws.relPkgsDir then
+  if !manifest.packages.isEmpty && manifest.packagesDir? != some (normalizePath 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)"
@@ -169,7 +186,7 @@ def Workspace.materializeDeps (ws : Workspace) (manifest : Manifest) (reconfigur
       let topLevel := pkg.name = ws.root.name
       let deps ← IO.ofExcept <| loadDepsFromEnv pkg.configEnv pkg.leanOpts
       if topLevel then
-        if manifest.isEmpty && !deps.isEmpty then
+        if manifest.packages.isEmpty && !deps.isEmpty then
           error "missing manifest; use `lake update` to generate one"
         for dep in deps do
           let warnOutOfDate (what : String) :=
@@ -185,19 +202,17 @@ def Workspace.materializeDeps (ws : Workspace) (manifest : Manifest) (reconfigur
           | _, _ => warnOutOfDate "source kind (git/path)"
       let depPkgs ← deps.mapM fun dep => fetchOrCreate dep.name do
         if let some entry := pkgEntries.find? dep.name then
-          let result ← entry.materialize ws.dir relPkgsDir ws.lakeEnv.pkgUrlMap
-          -- Union manifest and configuration options (preferring manifest)
-          let opts := entry.opts.mergeBy (fun _ e _ => e) dep.opts
-          result.loadPackage ws.dir pkg.leanOpts opts reconfigure
+          let result ← entry.materialize dep ws.dir relPkgsDir ws.lakeEnv.pkgUrlMap
+          result.loadPackage ws.dir pkg.leanOpts reconfigure
         else if topLevel then
           error <|
             s!"dependency '{dep.name}' not in manifest; " ++
             s!"use `lake update {dep.name}` to add it"
         else
           error <|
             s!"dependency '{dep.name}' of '{pkg.name}' not in manifest; " ++
-            s!"this suggests that the manifest is corrupt;" ++
-            s!"use `lake update` to generate a new, complete file (warning: this will update ALL workspace dependencies)"
+            "this suggests that the manifest is corrupt;" ++
+            "use `lake update` to generate a new, complete file (warning: this will update ALL workspace dependencies)"
       return {pkg with opaqueDeps := ← depPkgs.mapM (.mk <$> resolve ·)}
   match res with
   | Except.ok root =>