From 72ba52aec69ba71aa6e5347a3b10887487dd5f63 Mon Sep 17 00:00:00 2001 From: tydeu Date: Mon, 8 Jan 2024 12:19:12 -0500 Subject: [PATCH 1/2] feat: `lake update` from unsupported manifest versions --- src/lake/Lake/Load/Main.lean | 26 +++++++++++++---- src/lake/Lake/Load/Manifest.lean | 29 ++++++++++--------- src/lake/tests/manifest/lake-manifest-v4.json | 10 +++++++ src/lake/tests/manifest/test.sh | 28 ++++++++++++++---- 4 files changed, 67 insertions(+), 26 deletions(-) create mode 100644 src/lake/tests/manifest/lake-manifest-v4.json diff --git a/src/lake/Lake/Load/Main.lean b/src/lake/Lake/Load/Main.lean index d690610cf879..fbff001b4011 100644 --- a/src/lake/Lake/Load/Main.lean +++ b/src/lake/Lake/Load/Main.lean @@ -108,7 +108,8 @@ 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 @@ -116,8 +117,17 @@ def Workspace.updateAndMaterialize (ws : Workspace) 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 => + 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 +147,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 manifest '{depPkg.manifestFile}'" + | .error e => + logWarning s!"{depPkg.name}: ignoring manifest because it failed to load: {e}" modifyThe (NameMap Package) (·.insert dep.name depPkg) return depPkg -- Resolve dependencies's dependencies recursively @@ -236,8 +251,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 diff --git a/src/lake/Lake/Load/Manifest.lean b/src/lake/Lake/Load/Manifest.lean index 4335b48605a1..ab077fef29cc 100644 --- a/src/lake/Lake/Load/Manifest.lean +++ b/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. -/ diff --git a/src/lake/tests/manifest/lake-manifest-v4.json b/src/lake/tests/manifest/lake-manifest-v4.json new file mode 100644 index 000000000000..3b31f5bb5133 --- /dev/null +++ b/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"}}]} diff --git a/src/lake/tests/manifest/test.sh b/src/lake/tests/manifest/test.sh index 02282fe28ed8..e7cdd749f11b 100755 --- a/src/lake/tests/manifest/test.sh +++ b/src/lake/tests/manifest/test.sh @@ -21,29 +21,45 @@ git config user.name test git config user.email test@example.com 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 && false || true) | grep "incompatible manifest version '4'" + +# Test 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 From 2f8de0f9aafbe6fbf0cc8fdad23a7940396c3527 Mon Sep 17 00:00:00 2001 From: tydeu Date: Tue, 9 Jan 2024 22:02:04 -0500 Subject: [PATCH 2/2] chore: only ignore root manifest on a bare `lake update` --- src/lake/Lake/Load/Main.lean | 6 ++++-- src/lake/tests/manifest/test.sh | 7 +++++-- 2 files changed, 9 insertions(+), 4 deletions(-) diff --git a/src/lake/Lake/Load/Main.lean b/src/lake/Lake/Load/Main.lean index fbff001b4011..c865d7c3f2ba 100644 --- a/src/lake/Lake/Load/Main.lean +++ b/src/lake/Lake/Load/Main.lean @@ -127,6 +127,8 @@ def Workspace.updateAndMaterialize (ws : Workspace) | .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 @@ -154,9 +156,9 @@ def Workspace.updateAndMaterialize (ws : Workspace) let entry := entry.setInherited.inDirectory dep.relPkgDir modifyThe (NameMap PackageEntry) (·.insert entry.name entry) | .error (.noFileOrDirectory ..) => - logWarning s!"{depPkg.name}: ignoring missing manifest '{depPkg.manifestFile}'" + logWarning s!"{depPkg.name}: ignoring missing dependency manifest '{depPkg.manifestFile}'" | .error e => - logWarning s!"{depPkg.name}: ignoring manifest because it failed to load: {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 diff --git a/src/lake/tests/manifest/test.sh b/src/lake/tests/manifest/test.sh index e7cdd749f11b..be81297be044 100755 --- a/src/lake/tests/manifest/test.sh +++ b/src/lake/tests/manifest/test.sh @@ -32,9 +32,12 @@ LOCKED_REV='0538596b94a0510f55dc820cabd3bde41ad93c3e' # Test loading of a V4 manifest fails cp lake-manifest-v4.json lake-manifest.json -($LAKE resolve-deps 2>&1 && false || true) | grep "incompatible manifest version '4'" +($LAKE resolve-deps 2>&1 && exit 1 || true) | grep "incompatible manifest version '4'" -# Test update produces the expected V7 manifest +# 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