feat: lake update from unsupported manifest versions (#3149)

If the current manifest is from unsupported (or has errors), a bare
`lake update` will now discard it and create a new one from scratch
rather than erroring and requiring you to manually delete the manifest.
Lake will produce warnings noting it is ignoring such invalid manifests.

src/lake/Lake/Load/Main.lean

@@ -108,16 +108,28 @@ def Workspace.updateAndMaterialize (ws : Workspace)
   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
-    if let some manifest ← liftM <| Manifest.load? ws.manifestFile then
+    match (← Manifest.load ws.manifestFile |>.toBaseIO) with
+    | .ok manifest =>
       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
+          let doRename : IO Unit := do
+            createParentDirs ws.pkgsDir
+            IO.FS.rename oldPkgsDir ws.pkgsDir
+          if let .error e ← doRename.toBaseIO then
+            error <|
+              s!"{ws.root.name}: could not rename packages directory " ++
+              s!"({oldPkgsDir} -> {ws.pkgsDir}): {e}"
+    | .error (.noFileOrDirectory ..) =>
+      logInfo s!"{ws.root.name}: no previous manifest, creating one from scratch"
+    | .error e =>
+      unless toUpdate.isEmpty do
+        liftM (m := IO) <| throw e -- only ignore manifest on a bare `lake update`
+      logWarning s!"{ws.root.name}: ignoring previous manifest because it failed to load: {e}"
     buildAcyclic (·.name) ws.root fun pkg resolve => do
       let inherited := pkg.name != ws.root.name
       -- Materialize this package's dependencies first
@@ -137,11 +149,16 @@ def Workspace.updateAndMaterialize (ws : Workspace)
           if depPkg.name ≠ dep.name then
             logWarning s!"{pkg.name}: package '{depPkg.name}' was required as '{dep.name}'"
           -- Materialize locked dependencies
-          if let some manifest ← liftM <| Manifest.load? depPkg.manifestFile then
+          match (← Manifest.load depPkg.manifestFile |>.toBaseIO) with
+          | .ok manifest =>
             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)
+          | .error (.noFileOrDirectory ..) =>
+            logWarning s!"{depPkg.name}: ignoring missing dependency manifest '{depPkg.manifestFile}'"
+          | .error e =>
+            logWarning s!"{depPkg.name}: ignoring dependency manifest because it failed to load: {e}"
           modifyThe (NameMap Package) (·.insert dep.name depPkg)
           return depPkg
       -- Resolve dependencies's dependencies recursively
@@ -236,8 +253,7 @@ def loadWorkspace (config : LoadConfig) (updateDeps := false) : LogIO Workspace
   else
     ws.updateAndMaterialize {} rc
 
-
-/-- Updates the manifest for the loaded Lake workspace (see `buildUpdatedManifest`). -/
+/-- Updates the manifest for the loaded Lake workspace (see `updateAndMaterialize`). -/
 def updateManifest (config : LoadConfig) (toUpdate : NameSet := {}) : LogIO Unit := do
   let rc := config.reconfigure
   let ws ← loadWorkspaceRoot config

src/lake/Lake/Load/Manifest.lean

@@ -190,9 +190,9 @@ protected def fromJson? (json : Json) : Except String Manifest := do
     | throw "manifest not a JSON object"
   let ver : Json ← get obj "version"
   let .ok ver := ver.getNat?
-    | throw s!"unknown manifest version `{ver}`"
+    | throw s!"unknown manifest version '{ver}'"
   if ver < 5 then
-    throw s!"incompatible manifest version `{ver}`"
+    throw s!"incompatible manifest version '{ver}'"
   else if ver ≤ 6 then
     let name ← getD obj "name" Name.anonymous
     let lakeDir ← getD obj "lakeDir" defaultLakeDir
@@ -226,23 +226,24 @@ instance : FromJson Manifest := ⟨Manifest.fromJson?⟩
 /-- Parse a `Manifest` from a string. -/
 def parse (s : String) : Except String Manifest := do
   match Json.parse s with
-  | .ok json =>
-    match fromJson? json with
-    | .ok manifest => return manifest
-    | .error e => throw s!"improperly formatted manifest: {e}"
-  | .error e => throw s!"invalid JSON: {e}"
+  | .ok json => fromJson? json
+  | .error e => throw s!"manifest is not valid 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 the manifest file. Returns `none` if the file does not exist.
+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 (← IO.FS.readFile file |>.toBaseIO) with
-  | .ok contents =>
-    match inline <| Manifest.parse contents with
-    | .ok a => return some a
-    | .error e => error s!"{file}: {e}"
-  | .error (.noFileOrDirectory ..) => pure none
+  match (← inline (load file) |>.toBaseIO) with
+  | .ok contents => return contents
+  | .error (.noFileOrDirectory ..) => return none
   | .error e => throw e
 
 /-- Save the manifest as JSON to a file. -/

src/lake/tests/manifest/lake-manifest-v4.json

@@ -0,0 +1,10 @@
+{"version": 4,
+ "packagesDir": "lake-packages",
+ "packages":
+ [{"git":
+   {"url": "bar",
+    "subDir?": null,
+    "rev": "253735aaee71d8bb0f29ae5cfc3ce086a4b9e64f",
+    "name": "bar",
+    "inputRev?": null}},
+  {"path": {"opts": {}, "name": "foo", "inherited": false, "dir": "./foo"}}]}

src/lake/tests/manifest/test.sh

@@ -21,29 +21,48 @@ git config user.name test
 git config user.email [email protected]
 git add --all
 git commit -m "initial commit"
-REV=`git rev-parse HEAD`
+GIT_REV=`git rev-parse HEAD`
 popd
 
+LOCKED_REV='0538596b94a0510f55dc820cabd3bde41ad93c3e'
+
+# ---
+# Test manifest manually upgrades from unsupported versions
+# ---
+
+# Test loading of a V4 manifest fails
+cp lake-manifest-v4.json lake-manifest.json
+($LAKE resolve-deps 2>&1 && exit 1 || true) | grep "incompatible manifest version '4'"
+
+# Test package update fails as well
+($LAKE update bar 2>&1 && exit 1 || true) | grep "incompatible manifest version '4'"
+
+# Test bare update produces the expected V7 manifest
+$LAKE update
+sed_i "s/$GIT_REV/$LOCKED_REV/g" lake-manifest.json
+diff --strip-trailing-cr lake-manifest-v7.json lake-manifest.json
+rm -rf .lake
+
 # ---
-# Test manifest properly upgrades from supported versions
+# Test manifest automatically upgrades from supported versions
 # ---
 
 # Test successful loading of a V5 manifest
 cp lake-manifest-v5.json lake-manifest.json
-sed_i "s/253735aaee71d8bb0f29ae5cfc3ce086a4b9e64f/$REV/g" lake-manifest.json
+sed_i "s/253735aaee71d8bb0f29ae5cfc3ce086a4b9e64f/$GIT_REV/g" lake-manifest.json
 $LAKE resolve-deps
 
 # Test update produces the expected V7 manifest
 $LAKE update
-sed_i "s/$REV/0538596b94a0510f55dc820cabd3bde41ad93c3e/g" lake-manifest.json
+sed_i "s/$GIT_REV/$LOCKED_REV/g" lake-manifest.json
 diff --strip-trailing-cr lake-manifest-v7.json lake-manifest.json
 
 # Test successful loading of a V6 manifest
 cp lake-manifest-v6.json lake-manifest.json
-sed_i "s/dab525a78710d185f3d23622b143bdd837e44ab0/$REV/g" lake-manifest.json
+sed_i "s/dab525a78710d185f3d23622b143bdd837e44ab0/$GIT_REV/g" lake-manifest.json
 $LAKE resolve-deps
 
 # Test update produces the expected V7 manifest
 $LAKE update
-sed_i "s/$REV/0538596b94a0510f55dc820cabd3bde41ad93c3e/g" lake-manifest.json
+sed_i "s/$GIT_REV/$LOCKED_REV/g" lake-manifest.json
 diff --strip-trailing-cr lake-manifest-v7.json lake-manifest.json