From da61ae3a6c88ac09f6afd3e758d782b54849c3c0 Mon Sep 17 00:00:00 2001 From: Sebastian Graf Date: Fri, 6 Nov 2026 10:19:22 +0000 Subject: [PATCH] test: check `Sym` invariants in the `vcgen` tests Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01D74FF51DQwLT5S6Qt4iXvb --- tests/elab/10564.lean | 3 +++ tests/elab/11687.lean | 2 ++ tests/elab/12048.lean | 3 +++ tests/elab/9362.lean | 2 ++ tests/elab/9363.lean | 2 ++ tests/elab/9365.lean | 2 ++ tests/elab/9474.lean | 2 ++ tests/elab/9581.lean | 2 ++ tests/elab/bhaviksSampler.lean | 2 ++ tests/elab/bhaviksSampler.lean.out.expected | 12 ++++++------ tests/elab/doLogicTests.lean | 2 ++ tests/elab/experimentalIntrinsic.lean | 2 ++ tests/elab/forInListSpecUnivPoly.lean | 3 +++ tests/elab/grind_12246.lean | 2 ++ tests/elab/grind_12246.lean.out.expected | 6 +++--- tests/elab/mspecInvariantInstantiation.lean | 2 ++ tests/elab/mspecNoAssignSyntheticOpaque.lean | 2 ++ tests/elab/mvcgenInvariantsSuggestions.lean | 2 ++ tests/elab/mvcgenInvariantsWith.lean | 2 ++ tests/elab/mvcgenJPs.lean | 2 ++ tests/elab/mvcgenLocalSpec.lean | 2 ++ tests/elab/mvcgenPRangeInst.lean | 2 ++ tests/elab/mvcgenRflReducibility.lean | 2 ++ tests/elab/mvcgenSimpClassMethod.lean | 2 ++ tests/elab/mvcgenSplitState.lean | 2 ++ tests/elab/mvcgenTutorial.lean | 2 ++ tests/elab/mvcgenUnknownIdent.lean | 2 ++ tests/elab/mvcgenWithFail.lean | 2 ++ tests/elab/pairsSumToZero.lean | 2 ++ tests/elab/rc_model.lean | 2 ++ tests/elab/specInvariantAttr.lean | 2 ++ tests/elab/sym_intro_impl_detail.lean | 2 ++ tests/elab/sym_intro_issue.lean | 2 ++ tests/elab/sym_preprocessType_zetaDelta.lean | 2 ++ tests/elab/sym_simp_zeta.lean | 2 ++ tests/elab/vcgenCoinductiveFixpoint.lean | 2 ++ tests/elab/vcgenCondSplit.lean | 2 ++ tests/elab/vcgenDefeqAbuseProg.lean | 2 ++ tests/elab/vcgenDepAssertionLattice.lean | 2 ++ tests/elab/vcgenForallRhs.lean | 2 ++ tests/elab/vcgenHaveGoalMData.lean | 2 ++ tests/elab/vcgenImp.lean | 2 ++ tests/elab/vcgenLiftAnonymousTransformer.lean | 2 ++ tests/elab/vcgenMDataProgram.lean | 2 ++ tests/elab/vcgenMVarProgram.lean | 2 ++ tests/elab/vcgenMatchDependentDiscr.lean | 2 ++ tests/elab/vcgenMatchDiscrEq.lean | 2 ++ tests/elab/vcgenProgramBinderNames.lean | 2 ++ tests/elab/vcgenSchematicEPost.lean | 2 ++ tests/elab/vcgenSimp.lean | 2 ++ tests/elab/vcgenSpecAbbrev.lean | 2 ++ tests/elab/vcgenSpecInstDischarge.lean | 2 ++ tests/elab/vcgenSpecRuleCache.lean | 2 ++ tests/elab/vcgenStdDoGoal.lean | 2 ++ tests/elab/vcgenStdDoGoalStdWP.lean | 2 ++ tests/elab/vcgenSymBlock.lean | 2 ++ tests/elab/vcgenTermArgs.lean | 2 ++ tests/elab/vcgenToEStack.lean | 2 ++ tests/elab/vcgenUnfoldMatchDef.lean | 2 ++ tests/elab/vcgenUntil.lean | 2 ++ tests/elab/while_extrinsic.lean | 2 ++ 61 files changed, 130 insertions(+), 9 deletions(-) diff --git a/tests/elab/10564.lean b/tests/elab/10564.lean index 30cbb364e4dd..aedf9e03093e 100644 --- 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 index bbd8467a1cda..e4cc19f4a20e 100644 --- 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 index 838b7116d6a2..f97a6a5bf392 100644 --- 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 index 6c3372f2387b..2be0b243fa19 100644 --- 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 index 3c37dfc4d34f..14a87a894891 100644 --- 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 index f6e1243f153d..236fb0834aa8 100644 --- 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 index 9744bd99f2e7..778e4ba7f854 100644 --- 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 index 9991a43784a2..276be874e1f5 100644 --- 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 index 02b6add7e786..cc7716bb3eec 100644 --- 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 index 432c11c57d95..db09f4d7eac0 100644 --- 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 index 80cb509f2d7b..141f1d4772d4 100644 --- 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 index c966c1baf3de..62cca5c4ce49 100644 --- 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 index ba18698e666a..6e3b13a70d96 100644 --- 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 index 4b3beafd4495..d3953060a08b 100644 --- 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 index ae972eb91915..29184b1136e1 100644 --- 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 index 7bd369936544..157e8ff12dcd 100644 --- 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 index 297589eecfeb..318f9c62a745 100644 --- 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 index ee3c70c62d5d..dee7bf5725f7 100644 --- 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 index cf4b2194972e..30e2f1b40825 100644 --- 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 index 71575d235fdd..0c652c34b56a 100644 --- 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 index 8d48fe5b71bc..95ed0f6c24c3 100644 --- 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 index 539b40ff5dc2..4be139f53006 100644 --- 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 index 9611e076ea33..c841bd5ae4ec 100644 --- 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 index 32b85a750bda..54353980a4fe 100644 --- 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 index ab42f3794bfd..b2696f18ef85 100644 --- 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 index ca9fda42dc50..edb27b288d8f 100644 --- 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 index 7b6c1408c780..248dd68fb682 100644 --- 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 index 4807572f315a..253ddf2db4d4 100644 --- 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 index 68420ecea9a1..7df8f14e700b 100644 --- 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 index 38bc602431ad..d0a35bfeed6e 100644 --- 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 index 0484fba480b0..3d1e231b3b4d 100644 --- 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 index aacca61908f6..42f5a553bcc7 100644 --- 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 index 577f75290cb5..89db92a850bd 100644 --- 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 index f54867fad0a2..f0c3d89966bd 100644 --- 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 index e4cad4092be6..92df6e7bf18c 100644 --- 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 index c4c474b9cec4..17c5ebbc0a57 100644 --- 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 index 6f69ad049e5b..0a3f456642cf 100644 --- 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 index 90a89f1bea00..80a038623a78 100644 --- 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 index fdd505250878..7550702cf2b3 100644 --- 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 index 7f768f403aaa..a7df7de1a98f 100644 --- 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 index 4cbf15e376ea..7f450f57c783 100644 --- 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 index 9d1bad748013..9597e0925a65 100644 --- 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 index 5b3bf30345fd..db90bc845386 100644 --- 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 index 8e2982cf8587..3b0381e8dfb1 100644 --- 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 index b631dd194de3..ed8fa824602a 100644 --- 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 index 6b411a08f352..69d2f7f487a6 100644 --- 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 index 79d4208b5d6c..b1e9571d585f 100644 --- 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 diff --git a/tests/elab/vcgenProgramBinderNames.lean b/tests/elab/vcgenProgramBinderNames.lean index 48d0eb3adc07..1c14bc457cb1 100644 --- a/tests/elab/vcgenProgramBinderNames.lean +++ b/tests/elab/vcgenProgramBinderNames.lean @@ -1,5 +1,7 @@ import Std.WP +set_option sym.debug true + /-! Tests that `vcgen` names a loop's verification-condition binders after the program's own `for` element, mutable variable, and `invariant` clause binders rather than after the spec lemma's binders. The program's variables are accessible in the verification condition; the spec lemma's diff --git a/tests/elab/vcgenSchematicEPost.lean b/tests/elab/vcgenSchematicEPost.lean index 0d26120f3293..7387700c3e49 100644 --- a/tests/elab/vcgenSchematicEPost.lean +++ b/tests/elab/vcgenSchematicEPost.lean @@ -1,5 +1,7 @@ import Std.WP +set_option sym.debug true + /-! Tests that `vcgen` keeps the exception postcondition of a spec that states it as `estack⟨E⟩` with `E` schematic, that a spec stating `⊥` still weakens without emitting an exception postcondition diff --git a/tests/elab/vcgenSimp.lean b/tests/elab/vcgenSimp.lean index 16a3d92be0e1..df0fab57f24d 100644 --- a/tests/elab/vcgenSimp.lean +++ b/tests/elab/vcgenSimp.lean @@ -1,5 +1,7 @@ import Std.WP +set_option sym.debug true + /-! `vcgen` rewrites hypotheses, state arguments and verification conditions with its simp set: the `@[vcgen_simp]` theorems, the theorems of the `simp [...]` clause, and the evaluation of ground diff --git a/tests/elab/vcgenSpecAbbrev.lean b/tests/elab/vcgenSpecAbbrev.lean index b78eb4631e6f..fdccb94b7f8c 100644 --- a/tests/elab/vcgenSpecAbbrev.lean +++ b/tests/elab/vcgenSpecAbbrev.lean @@ -1,6 +1,8 @@ import Std.WP import Std.Tactic.Do +set_option sym.debug true + /-! Tests that `mvcgen` and `vcgen` apply a `@[spec]` theorem whose *type* is a reducible abbreviation wrapping a Hoare triple, e.g. `abbrev foo.spec := ⦃P⦄ foo ⦃Q⦄`. diff --git a/tests/elab/vcgenSpecInstDischarge.lean b/tests/elab/vcgenSpecInstDischarge.lean index edee6dab3589..74ce36fbccad 100644 --- a/tests/elab/vcgenSpecInstDischarge.lean +++ b/tests/elab/vcgenSpecInstDischarge.lean @@ -1,5 +1,7 @@ import Std.WP +set_option sym.debug true + /-! `vcgen` tries the `@[spec]` theorems matching a program in descending priority order and applies the first one whose backward rule applies. A spec guarded by an instance the call site does not provide diff --git a/tests/elab/vcgenSpecRuleCache.lean b/tests/elab/vcgenSpecRuleCache.lean index d54728258f7a..d00dfb2ab7f8 100644 --- a/tests/elab/vcgenSpecRuleCache.lean +++ b/tests/elab/vcgenSpecRuleCache.lean @@ -1,5 +1,7 @@ import Std.WP +set_option sym.debug true + /-! Regression test for `vcgen`'s spec backward-rule cache. The rule built from an equality spec must stay generic in the spec's value variables: the cache reuses the rule for every program matching diff --git a/tests/elab/vcgenStdDoGoal.lean b/tests/elab/vcgenStdDoGoal.lean index 2d7c20c6bc47..93b199251734 100644 --- a/tests/elab/vcgenStdDoGoal.lean +++ b/tests/elab/vcgenStdDoGoal.lean @@ -1,5 +1,7 @@ import Std.Tactic.Do +set_option sym.debug true + /-! `vcgen` explains how to migrate when the goal is a `Std.Do` triple and `Std.WP` is not imported (#15691). -/ diff --git a/tests/elab/vcgenStdDoGoalStdWP.lean b/tests/elab/vcgenStdDoGoalStdWP.lean index d8c46b1f9414..8660ba22761e 100644 --- a/tests/elab/vcgenStdDoGoalStdWP.lean +++ b/tests/elab/vcgenStdDoGoalStdWP.lean @@ -1,6 +1,8 @@ import Std.Tactic.Do import Std.WP +set_option sym.debug true + /-! `vcgen` explains how to migrate when the goal is a `Std.Do` triple and `Std.WP` is imported (#15691). -/ diff --git a/tests/elab/vcgenSymBlock.lean b/tests/elab/vcgenSymBlock.lean index 14f5a013a089..ac88e41eab0e 100644 --- a/tests/elab/vcgenSymBlock.lean +++ b/tests/elab/vcgenSymBlock.lean @@ -1,5 +1,7 @@ import Std.WP +set_option sym.debug true + /-! Tests that `vcgen` is usable as a step inside `sym => …` blocks. -/ open Std.WP Lean.Order diff --git a/tests/elab/vcgenTermArgs.lean b/tests/elab/vcgenTermArgs.lean index d0b237141b75..5cb9ee0223f8 100644 --- a/tests/elab/vcgenTermArgs.lean +++ b/tests/elab/vcgenTermArgs.lean @@ -1,5 +1,7 @@ import Std.WP +set_option sym.debug true + /-! Tests that `vcgen [...]` accepts arbitrary term arguments, mirroring `simp [...]`. A term proving a Hoare triple / `⊑ wp` spec is registered as a spec; any other proof is diff --git a/tests/elab/vcgenToEStack.lean b/tests/elab/vcgenToEStack.lean index ba851b0474e6..d604ee9ee51f 100644 --- a/tests/elab/vcgenToEStack.lean +++ b/tests/elab/vcgenToEStack.lean @@ -1,6 +1,8 @@ import Std.Tactic.Do import Std.WP +set_option sym.debug true + /-! `vcgen` weakens a concrete exception postcondition of a spec with pointwise verification conditions: for a bare `ε → Prop` such as the one of `Except ε`, and for a type such as `Thrown` diff --git a/tests/elab/vcgenUnfoldMatchDef.lean b/tests/elab/vcgenUnfoldMatchDef.lean index f2375b682b7e..235cf97347c5 100644 --- a/tests/elab/vcgenUnfoldMatchDef.lean +++ b/tests/elab/vcgenUnfoldMatchDef.lean @@ -1,5 +1,7 @@ import Std.WP +set_option sym.debug true + /-! Test for `vcgen [f]` where `f` is defined by a root `match` on its arguments. With an opaque discriminant the constructor equations cannot rewrite the call, so the unfold theorem `f.eq_def` diff --git a/tests/elab/vcgenUntil.lean b/tests/elab/vcgenUntil.lean index 4761a56336a4..878462b4a8fa 100644 --- a/tests/elab/vcgenUntil.lean +++ b/tests/elab/vcgenUntil.lean @@ -2,6 +2,8 @@ import Std.WP import Lean import Std +set_option sym.debug true + set_option experimental.vcgen true set_option warn.sorry false diff --git a/tests/elab/while_extrinsic.lean b/tests/elab/while_extrinsic.lean index c89b3bdb90ee..1c59846fbd71 100644 --- a/tests/elab/while_extrinsic.lean +++ b/tests/elab/while_extrinsic.lean @@ -2,6 +2,8 @@ module import Std +set_option sym.debug true + set_option linter.deprecated.syntax false open Std.Do