From f2d36227cf2e69b01e10e989d4eaf9643af6a1bd Mon Sep 17 00:00:00 2001 From: Sebastian Graf Date: Fri, 27 Mar 2026 12:29:26 +0100 Subject: [PATCH] chore: rename `mvcgen_invariant_type` attribute to `spec_invariant_type`, part 1 (#13153) This PR registers the new `spec_invariant_type` attribute alongside the old `mvcgen_invariant_type`, renames internal identifiers, and replaces the hardcoded `Invariant` check in `Spec.lean` with `isSpecInvariantType`. A follow-up PR will switch all usages to `spec_invariant_type` and remove the old attribute after stage0 is updated. Co-authored-by: Claude Opus 4.6 --- src/Lean/Elab/Tactic/Do/Attr.lean | 11 ++++++++--- src/Lean/Elab/Tactic/Do/Spec.lean | 9 +++++---- src/Lean/Elab/Tactic/Do/VCGen/Basic.lean | 2 +- stage0/src/stdlib_flags.h | 1 + 4 files changed, 15 insertions(+), 8 deletions(-) diff --git a/src/Lean/Elab/Tactic/Do/Attr.lean b/src/Lean/Elab/Tactic/Do/Attr.lean index 2d0040d874..eb32a1b1d5 100644 --- a/src/Lean/Elab/Tactic/Do/Attr.lean +++ b/src/Lean/Elab/Tactic/Do/Attr.lean @@ -256,15 +256,20 @@ Marks a type as an invariant type for the `mvcgen` tactic. Goals whose type is an application of a tagged type will be classified as invariants rather than verification conditions. -/ +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 `@[mvcgen_invariant_type]`. +Returns `true` if `ty` is an application of a type tagged with `@[spec_invariant_type]`. -/ -def isMVCGenInvariantType (env : Environment) (ty : Expr) : Bool := +def isSpecInvariantType (env : Environment) (ty : Expr) : Bool := if let .const name .. := ty.getAppFn then - mvcgenInvariantAttr.hasTag env name + specInvariantAttr.hasTag env name || mvcgenInvariantAttr.hasTag env name else false diff --git a/src/Lean/Elab/Tactic/Do/Spec.lean b/src/Lean/Elab/Tactic/Do/Spec.lean index 43083657b0..595a52c85c 100644 --- a/src/Lean/Elab/Tactic/Do/Spec.lean +++ b/src/Lean/Elab/Tactic/Do/Spec.lean @@ -75,7 +75,7 @@ def elabSpec (stx? : Option (TSyntax `term)) (wp : Expr) : TacticM SpecTheorem : | none => findSpec (← getSpecTheorems) wp | some stx => elabTermIntoSpecTheorem stx expectedTy -variable {n} [Monad n] [MonadControlT MetaM n] [MonadLiftT MetaM n] +variable {n} [Monad n] [MonadControlT MetaM n] [MonadLiftT MetaM n] [MonadEnv n] private def mkProj' (n : Name) (i : Nat) (Q : Expr) : MetaM Expr := do return (← projectCore? Q i).getD (mkProj n i Q) @@ -181,11 +181,12 @@ public def mSpec (goal : MGoal) (elabSpecAtWP : Expr → n SpecTheorem) (goalTag -- Instantiation creates `.natural` MVars, which possibly get instantiated by the def eq checks -- below when they occur in `P` or `Q`. -- That's good for many such as MVars ("schematic variables"), but problematic for MVars - -- corresponding to `Invariant`s, which should end up as user goals. - -- To prevent accidental instantiation, we mark all `Invariant` MVars as synthetic opaque. + -- corresponding to invariant types, which should end up as user goals. + -- To prevent accidental instantiation, we mark all invariant MVars as synthetic opaque. + let env ← getEnv for mvar in mvars do let ty ← mvar.mvarId!.getType - if ty.isAppOf ``Invariant then mvar.mvarId!.setKind .syntheticOpaque + if isSpecInvariantType env ty then mvar.mvarId!.setKind .syntheticOpaque -- Apply the spec to the excess arguments of the `wp⟦e⟧ Q` application let T := goal.target.consumeMData diff --git a/src/Lean/Elab/Tactic/Do/VCGen/Basic.lean b/src/Lean/Elab/Tactic/Do/VCGen/Basic.lean index 3b189f5e98..640fbfeb47 100644 --- a/src/Lean/Elab/Tactic/Do/VCGen/Basic.lean +++ b/src/Lean/Elab/Tactic/Do/VCGen/Basic.lean @@ -104,7 +104,7 @@ def addSubGoalAsVC (goal : MVarId) : VCGenM PUnit := do -- VC to the user as-is, without abstracting any variables in the local context. -- This only makes sense for synthetic opaque metavariables. goal.setKind .syntheticOpaque - if isMVCGenInvariantType (← getEnv) ty then + if isSpecInvariantType (← getEnv) ty then modify fun s => { s with invariants := s.invariants.push goal } else modify fun s => { s with vcs := s.vcs.push goal } diff --git a/stage0/src/stdlib_flags.h b/stage0/src/stdlib_flags.h index e444447049..691bde92ad 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 1/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.