comment out test

tests/lean/grind/casting.lean

@@ -0,0 +1,30 @@
+-- A simple proof that should go through immediately, gets stuck due to issues with casting Nat to Int.
+
+set_option grind.warning false
+@[grind] def codelen (c: List Bool) : Int := c.length
+
+/--
+error: `grind` failed
+case grind
+h : ¬codelen [] = 0
+⊢ False
+[grind] Goal diagnostics
+  [facts] Asserted facts
+    [prop] ¬codelen [] = 0
+    [prop] codelen [] = ↑[].length
+    [prop] [].length = 0
+  [eqc] False propositions
+    [prop] codelen [] = 0
+  [eqc] Equivalence classes
+    [eqc] {codelen [], ↑[].length}
+    [eqc] {[].length, 0}
+  [ematch] E-matching patterns
+    [thm] codelen.eq_1: [codelen #0]
+    [thm] List.length_nil: [@List.length #0 (@List.nil _)]
+[grind] Diagnostics
+  [thm] E-Matching instances
+    [thm] List.length_nil ↦ 1
+    [thm] codelen.eq_1 ↦ 1
+-/
+#guard_msgs in
+theorem issue1 : codelen [] = 0 := by grind

tests/lean/grind/product_eta.lean

@@ -0,0 +1,19 @@
+-- In nightly-2025-05-27 this leads to grind internal error "trying to assert equality c = (c.fst, c.snd) with proof Eq.refl c which has type c = c which is not definitionally equal with `reducible` transparency setting"
+
+set_option grind.warning false
+set_option grind.debug true
+
+
+def α : Type := Unit × Unit
+
+def p (_ : α) : Prop := False
+/--
+error: tactic 'grind.cases' failed, (non-recursive) inductive type expected at c
+  α
+case grind
+c : α
+h : p c
+⊢ False
+-/
+#guard_msgs in
+example : p c → False := by grind

tests/lean/run/grind_heartbeats.lean

@@ -11,15 +11,17 @@ macro_rules
   | `(gen! 0) => `(f 0)
   | `(gen! $n:num) => `(op (f $n) (gen! $(Lean.quote (n.getNat - 1))))
 
-/--
-trace: [grind.issues] (deterministic) timeout at `isDefEq`, maximum number of heartbeats (5000) has been reached
-    Use `set_option maxHeartbeats <num>` to set the limit.
-    ⏎
-    Additional diagnostic information may be available using the `set_option diagnostics true` command.
--/
-#guard_msgs (trace, drop error) in
-set_option trace.grind.issues true in
-set_option maxHeartbeats 5000 in
-example : gen! 10 = 0 ∧ True := by
-  set_option trace.Meta.debug true in
-  grind (instances := 10000)
+-- This test has been commented out as it is nondeterministic:
+-- sometimes it fails with a timeout at `whnf` rather than `isDefEq`.
+-- /--
+-- trace: [grind.issues] (deterministic) timeout at `isDefEq`, maximum number of heartbeats (5000) has been reached
+--     Use `set_option maxHeartbeats <num>` to set the limit.
+--     ⏎
+--     Additional diagnostic information may be available using the `set_option diagnostics true` command.
+-- -/
+-- #guard_msgs (trace, drop error) in
+-- set_option trace.grind.issues true in
+-- set_option maxHeartbeats 5000 in
+-- example : gen! 10 = 0 ∧ True := by
+--   set_option trace.Meta.debug true in
+--   grind (instances := 10000)