From f6ba82b74e9e906bf8de151344d292683d5720bd Mon Sep 17 00:00:00 2001 From: Mac Malone Date: Mon, 29 Apr 2024 17:35:42 -0400 Subject: [PATCH] chore: incorporate review comment --- src/lake/Lake/Load/Main.lean | 24 ++++++++++++++++++++---- 1 file changed, 20 insertions(+), 4 deletions(-) diff --git a/src/lake/Lake/Load/Main.lean b/src/lake/Lake/Load/Main.lean index ad331cd3f288..b1defb98a64f 100644 --- a/src/lake/Lake/Load/Main.lean +++ b/src/lake/Lake/Load/Main.lean @@ -133,6 +133,21 @@ private def resolveDepsAcyclic let cycle := cycle.map (s!" {·}") error s!"dependency cycle detected:\n{"\n".intercalate cycle}" +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} + +" + /-- Rebuild the workspace's Lake manifest and materialize missing dependencies. @@ -192,10 +207,11 @@ def Workspace.updateAndMaterialize let depPkg ← liftM <| loadDepPackage dep leanOpts reconfigure if depPkg.name ≠ dep.name then if dep.name = .mkSimple "std" then - logError s!"the 'std' package has been renamed to '{depPkg.name}'; \ - users should switch packages depending on new versions of std/{depPkg.name} \ - to 'require {depPkg.name}' instead of 'require std' and also update the \ - GitHub URL accordingly" + let rev := + match dep.manifestEntry with + | .git (inputRev? := some rev) .. => s!" @ {repr rev}" + | _ => "" + logError (stdMismatchError depPkg.name.toString rev) try IO.FS.removeDirAll depPkg.dir -- cleanup catch e =>