Skip to content

Commit

Permalink
chore: cache warns about bad v4.8.0-rc1 toolchain (#12623)
Browse files Browse the repository at this point in the history
Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
  • Loading branch information
semorrison and semorrison committed May 3, 2024
1 parent 9785488 commit e5e93cf
Showing 1 changed file with 4 additions and 0 deletions.
4 changes: 4 additions & 0 deletions Cache/Main.lean
Original file line number Diff line number Diff line change
Expand Up @@ -65,6 +65,10 @@ def leanTarArgs : List String :=

open Cache IO Hashing Requests System in
def main (args : List String) : IO Unit := do
if Lean.versionString == "4.8.0-rc1" && Lean.githash == "b470eb522bfd68ca96938c23f6a1bce79da8a99f" then do
println "Unfortunately, you have a broken Lean v4.8.0-rc1 installation."
println "Please run `elan toolchain uninstall leanprover/lean4:v4.8.0-rc1` and try again."
Process.exit 1
-- We pass any following arguments to `getHashMemo`,
-- so we can use the cache on `Archive` or `Counterexamples`.
let extraRoots := match args with
Expand Down

0 comments on commit e5e93cf

Please sign in to comment.