sgraf812 · Nov 6, 2026
diff --git a/tests/elab/10564.lean b/tests/elab/10564.lean
@@ -1,4 +1,7 @@
 import Std.Tactic.Do
+
+set_option sym.debug true
+
 open Std.Do
 
 set_option linter.deprecated.syntax false

diff --git a/tests/elab/11687.lean b/tests/elab/11687.lean
@@ -1,5 +1,7 @@
 import Std
 
+set_option sym.debug true
+
 set_option linter.deprecated.syntax false
 set_option warn.sorry false
 

diff --git a/tests/elab/12048.lean b/tests/elab/12048.lean
@@ -1,4 +1,7 @@
 import Std.Tactic.Do
+
+set_option sym.debug true
+
 open Std.Do
 
 set_option linter.deprecated.syntax false

diff --git a/tests/elab/9362.lean b/tests/elab/9362.lean
@@ -1,5 +1,7 @@
 import Std.Tactic.Do
 
+set_option sym.debug true
+
 open Std.Do
 
 set_option linter.deprecated.syntax false

diff --git a/tests/elab/9363.lean b/tests/elab/9363.lean
@@ -1,5 +1,7 @@
 import Std.Tactic.Do
 
+set_option sym.debug true
+
 open Std.Do
 
 set_option linter.deprecated.syntax false

diff --git a/tests/elab/9365.lean b/tests/elab/9365.lean
@@ -1,5 +1,7 @@
 import Std.Tactic.Do
 
+set_option sym.debug true
+
 open Std.Do
 
 set_option linter.deprecated.syntax false

diff --git a/tests/elab/9474.lean b/tests/elab/9474.lean
@@ -1,5 +1,7 @@
 import Std.Tactic.Do
 
+set_option sym.debug true
+
 open Std.Do
 
 set_option linter.deprecated.syntax false

diff --git a/tests/elab/9581.lean b/tests/elab/9581.lean
@@ -1,5 +1,7 @@
 import Std.Tactic.Do
 
+set_option sym.debug true
+
 open Std.Do
 
 set_option linter.deprecated.syntax false

diff --git a/tests/elab/bhaviksSampler.lean b/tests/elab/bhaviksSampler.lean
@@ -1,6 +1,8 @@
 import Std.Data.TreeMap
 import Std.Tactic.Do
 
+set_option sym.debug true
+
 /-!
 This test is based on code by Bhavik Mehta.
 It demonstrates that much of the boilerplate that he was forced to write for his proof

diff --git a/tests/elab/bhaviksSampler.lean.out.expected b/tests/elab/bhaviksSampler.lean.out.expected
@@ -1,6 +1,6 @@
-bhaviksSampler.lean:97:4-97:11: warning: declaration uses `sorry`
-bhaviksSampler.lean:116:4-116:8: warning: declaration uses `sorry`
-bhaviksSampler.lean:125:8-125:18: warning: declaration uses `sorry`
-bhaviksSampler.lean:128:8-128:25: warning: declaration uses `sorry`
-bhaviksSampler.lean:155:17-155:24: warning: declaration uses `sorry`
-bhaviksSampler.lean:151:8-151:23: warning: declaration uses `sorry`
+bhaviksSampler.lean:99:4-99:11: warning: declaration uses `sorry`
+bhaviksSampler.lean:118:4-118:8: warning: declaration uses `sorry`
+bhaviksSampler.lean:127:8-127:18: warning: declaration uses `sorry`
+bhaviksSampler.lean:130:8-130:25: warning: declaration uses `sorry`
+bhaviksSampler.lean:157:17-157:24: warning: declaration uses `sorry`
+bhaviksSampler.lean:153:8-153:23: warning: declaration uses `sorry`
diff --git a/tests/elab/doLogicTests.lean b/tests/elab/doLogicTests.lean
@@ -8,6 +8,8 @@ import Std
 import Lean.Elab.Tactic.Do.VCGen
 import Lean
 
+set_option sym.debug true
+
 open Std.Do
 
 set_option grind.warning false

diff --git a/tests/elab/experimentalIntrinsic.lean b/tests/elab/experimentalIntrinsic.lean
@@ -1,5 +1,7 @@
 import Std.WP
 
+set_option sym.debug true
+
 /-!
 Every form of the intrinsic verification syntax reports that it is experimental, at the keyword that
 introduces the form, and `set_option experimental.intrinsic true` silences those reports.

diff --git a/tests/elab/forInListSpecUnivPoly.lean b/tests/elab/forInListSpecUnivPoly.lean
@@ -1,4 +1,7 @@
 import Std.Tactic.Do
+
+set_option sym.debug true
+
 open Std.Do
 set_option linter.deprecated.syntax false
 set_option warn.sorry false

diff --git a/tests/elab/grind_12246.lean b/tests/elab/grind_12246.lean
@@ -1,6 +1,8 @@
 import Std.Do
 import Std.Tactic.Do
 
+set_option sym.debug true
+
 def Matrix' (α β γ : Type) : Type := α → β → γ
 
 namespace Matrix'

diff --git a/tests/elab/grind_12246.lean.out.expected b/tests/elab/grind_12246.lean.out.expected
@@ -1,3 +1,3 @@
-grind_12246.lean:11:4-11:15: warning: declaration uses `sorry`
-grind_12246.lean:14:4-14:14: warning: declaration uses `sorry`
-grind_12246.lean:30:8-30:29: warning: declaration uses `sorry`
+grind_12246.lean:13:4-13:15: warning: declaration uses `sorry`
+grind_12246.lean:16:4-16:14: warning: declaration uses `sorry`
+grind_12246.lean:32:8-32:29: warning: declaration uses `sorry`
diff --git a/tests/elab/mspecInvariantInstantiation.lean b/tests/elab/mspecInvariantInstantiation.lean
@@ -1,6 +1,8 @@
 import Std.Tactic.Do
 import Std.Do.WP.Basic
 
+set_option sym.debug true
+
 def tst (n : Nat) : Vector Bool n := Id.run do
   let mut res : Vector Bool n := .ofFn fun _ ↦ false
   for i in [:n] do

diff --git a/tests/elab/mspecNoAssignSyntheticOpaque.lean b/tests/elab/mspecNoAssignSyntheticOpaque.lean
@@ -1,5 +1,7 @@
 import Lean
 
+set_option sym.debug true
+
 open Std.Do
 
 set_option linter.deprecated.syntax false

diff --git a/tests/elab/mvcgenInvariantsSuggestions.lean b/tests/elab/mvcgenInvariantsSuggestions.lean
@@ -1,6 +1,8 @@
 import Std.Tactic.Do
 import Std
 
+set_option sym.debug true
+
 open Std Do
 
 set_option grind.warning false

diff --git a/tests/elab/mvcgenInvariantsWith.lean b/tests/elab/mvcgenInvariantsWith.lean
@@ -1,6 +1,8 @@
 import Std.Tactic.Do
 import Std
 
+set_option sym.debug true
+
 open Std Do
 
 set_option grind.warning false

diff --git a/tests/elab/mvcgenJPs.lean b/tests/elab/mvcgenJPs.lean
@@ -1,5 +1,7 @@
 import Std.Tactic.Do
 
+set_option sym.debug true
+
 open Std.Do
 
 set_option grind.warning false

diff --git a/tests/elab/mvcgenLocalSpec.lean b/tests/elab/mvcgenLocalSpec.lean
@@ -1,5 +1,7 @@
 import Std.Tactic.Do
 
+set_option sym.debug true
+
 open Std.Do
 
 set_option linter.deprecated.syntax false

diff --git a/tests/elab/mvcgenPRangeInst.lean b/tests/elab/mvcgenPRangeInst.lean
@@ -1,5 +1,7 @@
 import Std.Tactic.Do
 
+set_option sym.debug true
+
 open Std.Do
 
 set_option warn.sorry false

diff --git a/tests/elab/mvcgenRflReducibility.lean b/tests/elab/mvcgenRflReducibility.lean
@@ -1,5 +1,7 @@
 import Std.Tactic.Do
 
+set_option sym.debug true
+
 /-!
 This test case from Hax asserts that `mspec` doesn't use default reducibility when trying
 `SPred.entails.rfl`. If it did, then the `MyShl.shl a 32` would be unfolded deeply and we'd run

diff --git a/tests/elab/mvcgenSimpClassMethod.lean b/tests/elab/mvcgenSimpClassMethod.lean
@@ -1,5 +1,7 @@
 import Std.Tactic.Do
 
+set_option sym.debug true
+
 open Std.Do
 
 set_option linter.deprecated.syntax false

diff --git a/tests/elab/mvcgenSplitState.lean b/tests/elab/mvcgenSplitState.lean
@@ -1,5 +1,7 @@
 import Std.Tactic.Do
 
+set_option sym.debug true
+
 open Std.Do
 
 /-!

diff --git a/tests/elab/mvcgenTutorial.lean b/tests/elab/mvcgenTutorial.lean
@@ -2,6 +2,8 @@ import Std.Tactic.Do
 import Std.Tactic.BVDecide
 import Std.Data.HashSet
 
+set_option sym.debug true
+
 set_option grind.warning false
 set_option linter.deprecated.syntax false
 

diff --git a/tests/elab/mvcgenUnknownIdent.lean b/tests/elab/mvcgenUnknownIdent.lean
@@ -1,5 +1,7 @@
 import Std.Tactic.Do
 
+set_option sym.debug true
+
 open Std.Do
 
 set_option linter.deprecated.syntax false

diff --git a/tests/elab/mvcgenWithFail.lean b/tests/elab/mvcgenWithFail.lean
@@ -1,5 +1,7 @@
 import Std
 
+set_option sym.debug true
+
 /-!
   `mvcgen with grind` should behave like `induction ... with grind` and fail if `grind` fails on
   one of the goals.

diff --git a/tests/elab/pairsSumToZero.lean b/tests/elab/pairsSumToZero.lean
@@ -6,6 +6,8 @@ https://markushimmel.de/blog/my-first-verified-imperative-program/
 import Std.Data.HashSet.Lemmas
 import Std.Tactic.Do
 
+set_option sym.debug true
+
 open Std Do
 
 /-!

diff --git a/tests/elab/rc_model.lean b/tests/elab/rc_model.lean
@@ -1,6 +1,8 @@
 import Std.Tactic.BVDecide
 import Std.Tactic.Do
 
+set_option sym.debug true
+
 open Std Do
 
 set_option doc.verso true

diff --git a/tests/elab/specInvariantAttr.lean b/tests/elab/specInvariantAttr.lean
@@ -1,6 +1,8 @@
 import Std.Tactic.Do
 import Std
 
+set_option sym.debug true
+
 open Std Do
 
 set_option grind.warning false

diff --git a/tests/elab/sym_intro_impl_detail.lean b/tests/elab/sym_intro_impl_detail.lean
@@ -1,6 +1,8 @@
 import Std.WP
 import Std.Tactic.Do
 
+set_option sym.debug true
+
 /-!
 `sym => intro` introduces a binder whose name starts with `__` as an implementation-detail local,
 as the elaborator does for such binders, so the goal hides it. `vcgen` introduces the join point

diff --git a/tests/elab/sym_intro_issue.lean b/tests/elab/sym_intro_issue.lean
@@ -12,6 +12,8 @@ Fix: guard `finalize` with `if fvars.isEmpty then return (#[], mvarId)`.
 -/
 import Lean
 
+set_option sym.debug true
+
 -- Demonstrate the bug by calling `Sym.intros` on a non-forall goal.
 -- With the fix in `introCore.finalize`, this prints "GOOD".
 -- Without the fix, it prints "BUG".

diff --git a/tests/elab/sym_preprocessType_zetaDelta.lean b/tests/elab/sym_preprocessType_zetaDelta.lean
@@ -1,5 +1,7 @@
 import Lean.Meta.Sym
 
+set_option sym.debug true
+
 /-!
 `Sym.preprocessType` must not zeta-delta ambient let-bound fvars unless explicitly
 requested (`zetaDelta := false` by default). Regression test from Sebastian Graf's

diff --git a/tests/elab/sym_simp_zeta.lean b/tests/elab/sym_simp_zeta.lean
@@ -1,5 +1,7 @@
 import Std.Tactic.Do
 
+set_option sym.debug true
+
 /-!
 `Sym.simp` rewrite theorems must preserve nondep `let`s (e.g. do-notation `__do_jp`
 join points) in their RHS. Previously `preprocessType` zeta-reduced the whole theorem

diff --git a/tests/elab/vcgenCoinductiveFixpoint.lean b/tests/elab/vcgenCoinductiveFixpoint.lean
@@ -1,5 +1,7 @@
 import Std.WP
 
+set_option sym.debug true
+
 /-!
 # `coinductive_fixpoint` beside a `vcgen` proof
 

diff --git a/tests/elab/vcgenCondSplit.lean b/tests/elab/vcgenCondSplit.lean
@@ -1,5 +1,7 @@
 import Std.WP
 
+set_option sym.debug true
+
 /-!
 `vcgen` splits a program headed by `cond` (`bif c then t else e`) into one verification
 condition per branch, with `c = true` or `c = false` in scope. The split rule is cached

diff --git a/tests/elab/vcgenDefeqAbuseProg.lean b/tests/elab/vcgenDefeqAbuseProg.lean
@@ -1,6 +1,8 @@
 import Std.WP
 import Std.WP.Triple.SpecLemmas
 
+set_option sym.debug true
+
 /-!
 # `vcgen` on a program that is not of the type of its `WP` instance
 

diff --git a/tests/elab/vcgenDepAssertionLattice.lean b/tests/elab/vcgenDepAssertionLattice.lean
@@ -1,5 +1,7 @@
 import Std.WP
 
+set_option sym.debug true
+
 /-!
 Regression test for a *dependent* assertion language `(st : State) → st.Invariant → Prop`. Its order
 is the pointwise function order, but `vcgen`'s peel rule `le_of_forall_le` cannot currently be

diff --git a/tests/elab/vcgenForallRhs.lean b/tests/elab/vcgenForallRhs.lean
@@ -1,5 +1,7 @@
 import Std.WP
 
+set_option sym.debug true
+
 /-!
 `vcgen` must split a raw `∀`/`→` on the RHS of a `Prop` entailment (`le_forall`) and an `iInf` on
 any `Pi` assertion lattice (`iInf_apply` + `le_iInf`), including when the `iInf` is applied to excess

diff --git a/tests/elab/vcgenHaveGoalMData.lean b/tests/elab/vcgenHaveGoalMData.lean
@@ -1,5 +1,7 @@
 import Std.WP
 
+set_option sym.debug true
+
 /-! A tactic `have`/`let`/`suffices` wraps the goal in `noImplicitLambda` `mdata` (via
 `refine_lift no_implicit_lambda% …`). `vcgen` must read the program type through that annotation.
 Also checks that `⦃…⦄` elaborates with only `open Std.WP` (no `open Lean.Order`). -/

diff --git a/tests/elab/vcgenImp.lean b/tests/elab/vcgenImp.lean
@@ -6,6 +6,8 @@ Authors: Sebastian Graf
 import Std.WP
 import Std.WP.Triple.SpecLemmas
 
+set_option sym.debug true
+
 /-!
 # `vcgen` on a non-monadic program type
 

diff --git a/tests/elab/vcgenLiftAnonymousTransformer.lean b/tests/elab/vcgenLiftAnonymousTransformer.lean
@@ -1,5 +1,7 @@
 import Std.WP
 
+set_option sym.debug true
+
 /-!
 `liftMach` coerces the anonymous state transformer `fun s => match c s.machine with …` into
 `EStateM Unit Sys` by definitional unfolding alone: `EStateM` is a reducible function type, so

diff --git a/tests/elab/vcgenMDataProgram.lean b/tests/elab/vcgenMDataProgram.lean
@@ -2,6 +2,8 @@ import Std.WP
 import Lean
 import Std
 
+set_option sym.debug true
+
 set_option experimental.vcgen true
 
 /-! `vcgen` must classify a program wrapped in an `mdata` node, such as the

diff --git a/tests/elab/vcgenMVarProgram.lean b/tests/elab/vcgenMVarProgram.lean
@@ -1,5 +1,7 @@
 import Std.WP
 
+set_option sym.debug true
+
 /-!
 A spec whose program applies a continuation variable under a binder, as in
 `Lang.bnd (fun x => Lang.add (k x) (Lang.nat 0))`. First-order matching leaves `k` open, so

diff --git a/tests/elab/vcgenMatchDependentDiscr.lean b/tests/elab/vcgenMatchDependentDiscr.lean
@@ -1,6 +1,8 @@
 import Std.Tactic.Do
 import Std.WP
 
+set_option sym.debug true
+
 /-!
 Regression test for `mvcgen`/`vcgen` splitting a `match` whose discriminant telescope is
 dependent: a later discriminant's type mentions an earlier discriminant. Abstracting the matcher

diff --git a/tests/elab/vcgenMatchDiscrEq.lean b/tests/elab/vcgenMatchDiscrEq.lean
@@ -1,6 +1,8 @@
 import Std.Tactic.Do
 import Std.WP
 
+set_option sym.debug true
+
 /-!
 Regression test for `vcgen` splitting a `match h : d with` whose alternatives bind an equality
 `h : d = pattern`. The split must not substitute the discriminant in the alternatives, since their