Bump to Lean v4.10.0

One of the new core linters crashes on this test, so for now we disable it. Since we're touching the test anyway, let's improve the output checking.
leanprover-community · Aug 9, 2024 · 8e20e08 · 8e20e08
1 parent 01ad339
commit 8e20e08
Show file tree

Hide file tree

Showing 2 changed files with 7 additions and 2 deletions.
diff --git a/examples/hoMatching.lean b/examples/hoMatching.lean
@@ -1,8 +1,13 @@
 import Qq
 open Qq Lean
 
+-- TODO: this linter crashes on the `def` below
+set_option linter.constructorNameAsVariable false in
 def turnExistsIntoForall : Q(Prop) → MetaM Q(Prop)
   | ~q(∃ x y, $p x y) => return q(∀ x y, $p x y)
   | e => return e
 
-#eval turnExistsIntoForall q(∃ a b, String.length a ≤ b + 42)
+/-- info: ∀ (x : String) (y : Nat), x.length ≤ y + 42 -/
+#guard_msgs in
+run_cmd Elab.Command.liftTermElabM do
+  Lean.logInfo <| ← turnExistsIntoForall q(∃ a b, String.length a ≤ b + 42)
diff --git a/lean-toolchain b/lean-toolchain
@@ -1 +1 @@
-leanprover/lean4:v4.9.0-rc1
+leanprover/lean4:v4.10.0