From 938c19aace99b7a79cc215578eeef84784780b47 Mon Sep 17 00:00:00 2001 From: Sebastian Graf Date: Fri, 27 Mar 2026 14:06:17 +0100 Subject: [PATCH] chore: rename `mvcgen_invariant_type` attribute to `spec_invariant_type`, part 2 (#13157) This PR switches all usages from `@[mvcgen_invariant_type]` to `@[spec_invariant_type]` and removes the old attribute registration. Concludes the work of #13153. Co-authored-by: Claude Opus 4.6 --- src/Lean/Elab/Tactic/Do/Attr.lean | 7 +------ src/Std/Do/Triple/SpecLemmas.lean | 6 +++--- stage0/src/stdlib_flags.h | 1 + .../{mvcgenInvariantAttr.lean => specInvariantAttr.lean} | 6 +++--- 4 files changed, 8 insertions(+), 12 deletions(-) rename tests/elab/{mvcgenInvariantAttr.lean => specInvariantAttr.lean} (89%) diff --git a/src/Lean/Elab/Tactic/Do/Attr.lean b/src/Lean/Elab/Tactic/Do/Attr.lean index eb32a1b1d5..9645e42158 100644 --- a/src/Lean/Elab/Tactic/Do/Attr.lean +++ b/src/Lean/Elab/Tactic/Do/Attr.lean @@ -260,16 +260,11 @@ builtin_initialize specInvariantAttr : TagAttribute ← registerTagAttribute `spec_invariant_type "marks a type as an invariant type for the `mvcgen` tactic" --- Keep old attribute name temporarily for bootstrapping; removed after stage0 update. -builtin_initialize mvcgenInvariantAttr : TagAttribute ← - registerTagAttribute `mvcgen_invariant_type - "marks a type as an invariant type for the `mvcgen` tactic" - /-- Returns `true` if `ty` is an application of a type tagged with `@[spec_invariant_type]`. -/ def isSpecInvariantType (env : Environment) (ty : Expr) : Bool := if let .const name .. := ty.getAppFn then - specInvariantAttr.hasTag env name || mvcgenInvariantAttr.hasTag env name + specInvariantAttr.hasTag env name else false diff --git a/src/Std/Do/Triple/SpecLemmas.lean b/src/Std/Do/Triple/SpecLemmas.lean index 48a27fa976..0323db2408 100644 --- a/src/Std/Do/Triple/SpecLemmas.lean +++ b/src/Std/Do/Triple/SpecLemmas.lean @@ -697,7 +697,7 @@ After leaving the loop, the cursor's prefix is `xs` and the suffix is empty. During the induction step, the invariant holds for a suffix with head element `x`. After running the loop body, the invariant then holds after shifting `x` to the prefix. -/ -@[mvcgen_invariant_type] +@[spec_invariant_type] abbrev Invariant {α : Type u₁} (xs : List α) (β : Type u₂) (ps : PostShape.{max u₁ u₂}) := PostCond (List.Cursor xs × β) ps @@ -2027,7 +2027,7 @@ A loop invariant is a `PostCond` that takes as parameters * A state tuple of type `β`, which will be a nesting of `MProd`s representing the elaboration of `let mut` variables and early return. -/ -@[mvcgen_invariant_type] +@[spec_invariant_type] abbrev StringInvariant (s : String) (β : Type u) (ps : PostShape.{u}) := PostCond (s.Pos × β) ps @@ -2112,7 +2112,7 @@ A loop invariant is a `PostCond` that takes as parameters * A state tuple of type `β`, which will be a nesting of `MProd`s representing the elaboration of `let mut` variables and early return. -/ -@[mvcgen_invariant_type] +@[spec_invariant_type] abbrev StringSliceInvariant (s : String.Slice) (β : Type u) (ps : PostShape.{u}) := PostCond (s.Pos × β) ps diff --git a/stage0/src/stdlib_flags.h b/stage0/src/stdlib_flags.h index e444447049..6168fbec34 100644 --- a/stage0/src/stdlib_flags.h +++ b/stage0/src/stdlib_flags.h @@ -22,6 +22,7 @@ options get_default_options() { opts = opts.update({"quotPrecheck"}, true); opts = opts.update({"pp", "rawOnError"}, true); + // update stage0 for spec_invariant_type attribute rename (step 2/2) // Temporary, core-only flags for editing (i.e. must be part of stage0/bin/lean). Must be synced // with `LEAN_EXTRA_MAKE_OPTS` build flags in src/CMakeLists.txt. diff --git a/tests/elab/mvcgenInvariantAttr.lean b/tests/elab/specInvariantAttr.lean similarity index 89% rename from tests/elab/mvcgenInvariantAttr.lean rename to tests/elab/specInvariantAttr.lean index 5acfa31be2..8d61cf0aa6 100644 --- a/tests/elab/mvcgenInvariantAttr.lean +++ b/tests/elab/specInvariantAttr.lean @@ -7,11 +7,11 @@ open Std Do set_option grind.warning false set_option mvcgen.warning false --- Test that `@[mvcgen_invariant_type]` works end-to-end with a custom invariant type. +-- Test that `@[spec_invariant_type]` works end-to-end with a custom invariant type. -- We replicate the `StringInvariant` setup locally: define a type, tag it, provide a spec, -- and verify that `mvcgen` classifies the invariant goal as `inv1` rather than `vc1`. -@[mvcgen_invariant_type] +@[spec_invariant_type] abbrev MyStringInvariant (s : String) (β : Type u) (ps : PostShape.{u}) := PostCond (s.Pos × β) ps @@ -43,7 +43,7 @@ def stringLoop (s : String) : Id Unit := do theorem stringLoop_correct (s : String) : ⦃⌜True⌝⦄ stringLoop s ⦃⇓ _ => ⌜True⌝⦄ := by - -- With `@[mvcgen_invariant_type]` on `MyStringInvariant`, mvcgen classifies the + -- With `@[spec_invariant_type]` on `MyStringInvariant`, mvcgen classifies the -- loop invariant goal as `inv1` rather than `vc1`, enabling the `invariants` syntax. mvcgen [stringLoop] invariants · ⇓ _ => ⌜True⌝