From ad1c983a43face43c3e69b72f7db105f40ef280a Mon Sep 17 00:00:00 2001 From: Kyle Miller Date: Thu, 21 May 2026 12:45:59 -0700 Subject: [PATCH] fix: run beforeElaboration attributes on inductives (#13813) This PR fixes an issue where `beforeElaboration` attributes were not being run on `inductive`/`structure`/`coinductive` commands. Closes #13433. There is also light refactoring of MutualInductive, as well as a mild performance enhancement to avoid repeated re-elaboration of `variable`s. --- src/Lean/Elab/MutualInductive.lean | 61 ++++++--------------- tests/pkg/user_attr/UserAttr/BlaAttr.lean | 28 ++++++++++ tests/pkg/user_attr/UserAttr/Tst.lean | 65 +++++++++++++++++++++++ 3 files changed, 110 insertions(+), 44 deletions(-) diff --git a/src/Lean/Elab/MutualInductive.lean b/src/Lean/Elab/MutualInductive.lean index 2991bae5f1..70ed2def6e 100644 --- a/src/Lean/Elab/MutualInductive.lean +++ b/src/Lean/Elab/MutualInductive.lean @@ -1595,14 +1595,14 @@ private def elabFlatInductiveViews (vars : Array Expr) (elabs : Array InductiveE enableRealizationsForConst e.view.declName /-- Ensures that there are no conflicts among or between the type and constructor names defined in `elabs`. -/ -private def checkNoInductiveNameConflicts (elabs : Array InductiveElabStep1) (isCoinductive : Bool := false) : TermElabM Unit := do - let throwErrorsAt (init cur : Syntax) (msg : MessageData) : TermElabM Unit := do +private def checkNoInductiveNameConflicts (elabs : Array InductiveElabStep1) (isCoinductive : Bool := false) : CommandElabM Unit := do + let throwErrorsAt (init cur : Syntax) (msg : MessageData) : CommandElabM Unit := do logErrorAt init msg throwErrorAt cur msg -- Maps names of inductive types to `true` and those of constructors to `false`, along with syntax refs let mut uniqueNames : Std.HashMap Name (Bool × Syntax) := {} let declString := if isCoinductive then "coinductive predicate" else "inductive type" - trace[Elab.inductive] "deckString: {declString}" + trace[Elab.inductive] "declString: {declString}" for { view, .. } in elabs do let typeDeclName := privateToUserName view.declName if let some (prevNameIsType, prevRef) := uniqueNames[typeDeclName]? then @@ -1656,46 +1656,23 @@ private def applyDerivingHandlers (views : Array InductiveView) : CommandElabM U declNames := declNames.push view.declName classView.applyHandlers declNames -private def elabInductiveViewsPostprocessing (views : Array InductiveView) (res : FinalizeContext) - : CommandElabM Unit := do - let view0 := views[0]! - let ref := view0.ref +private def elabInductiveViewsFinalize (views : Array InductiveView) (res : FinalizeContext) : + CommandElabM Unit := do applyComputedFields views -- NOTE: any generated code before this line is invalid liftTermElabM <| withMCtx res.mctx <| withLCtx res.lctx res.localInsts do let finalizers ← res.elabs.mapM fun elab' => elab'.prefinalize res.levelParams res.params res.replaceIndFVars for view in views do withRef view.declId <| Term.applyAttributesAt view.declName view.modifiers.attrs .afterTypeChecking for elab' in finalizers do elab'.finalize - applyDerivingHandlers views - -- Docstrings are added during postprocessing to allow them to have checked references to - -- the type and its constructors, but before attributes to enable e.g. `@[inherit_doc X]` - runTermElabM fun _ => Term.withDeclName view0.declName do withRef ref do - for view in views do - withRef view.declId do - if let some (doc, verso) := view.docString? then - addDocStringOf verso view.declName view.binders doc - for ctor in view.ctors do - withRef ctor.declId do - if let some (doc, verso) := ctor.modifiers.docString? then - addDocStringOf verso ctor.declName ctor.binders doc - runTermElabM fun _ => Term.withDeclName view0.declName do withRef ref do - for view in views do withRef view.declId <| - unless (views.any (·.isCoinductive)) do - Term.applyAttributesAt view.declName view.modifiers.attrs .afterCompilation - - -- Term info is added here so that docstrings are maximally available in the environment for hovers - runTermElabM fun _ => Term.withDeclName view0.declName <| withRef ref <| addTermInfoViews views - -private def elabInductiveViewsPostprocessingCoinductive (views : Array InductiveView) - : CommandElabM Unit := do +private def elabInductiveViewsPostprocessing (views : Array InductiveView) : + CommandElabM Unit := do let view0 := views[0]! let ref := view0.ref - applyDerivingHandlers views -- Docstrings are added during postprocessing to allow them to have checked references to -- the type and its constructors, but before attributes to enable e.g. `@[inherit_doc X]` - runTermElabM fun _ => Term.withDeclName view0.declName do withRef ref do + liftTermElabM <| Term.withDeclName view0.declName do withRef ref do for view in views do withRef view.declId do if let some (doc, verso) := view.docString? then @@ -1705,13 +1682,12 @@ private def elabInductiveViewsPostprocessingCoinductive (views : Array Inductive if let some (doc, verso) := ctor.modifiers.docString? then addDocStringOf verso ctor.declName ctor.binders doc - runTermElabM fun _ => Term.withDeclName view0.declName do withRef ref do for view in views do withRef view.declId <| unless (views.any (·.isCoinductive)) do Term.applyAttributesAt view.declName view.modifiers.attrs .afterCompilation - -- Term info is added here so that docstrings are maximally available in the environment for hovers - runTermElabM fun _ => Term.withDeclName view0.declName <| withRef ref <| addTermInfoViews views + -- Term info is added here so that docstrings are maximally available in the environment for hovers + addTermInfoViews views def InductiveViewToCoinductiveElab (e : InductiveElabStep1) : CoinductiveElabData where declId := e.view.declId @@ -1722,26 +1698,23 @@ def InductiveViewToCoinductiveElab (e : InductiveElabStep1) : CoinductiveElabDat isGreatest := e.view.isCoinductive def elabInductives (inductives : Array (Modifiers × Syntax)) : CommandElabM Unit := do - let elabs ← runTermElabM fun _ => - inductives.mapM fun (modifiers, stx) => mkInductiveView modifiers stx - + let elabs ← runTermElabM fun _ => inductives.mapM fun (modifiers, stx) => mkInductiveView modifiers stx let isCoinductive := elabs.any (·.view.isCoinductive) - + checkNoInductiveNameConflicts elabs (isCoinductive := isCoinductive) + elabs.forM fun e => checkValidInductiveModifier e.view.modifiers + liftTermElabM <| elabs.forM fun e => withRef e.view.ref do + Term.applyAttributesAt e.view.declName e.view.modifiers.attrs .beforeElaboration if isCoinductive then runTermElabM fun vars => do - checkNoInductiveNameConflicts elabs (isCoinductive := true) let flatElabs := elabs.map fun e => {e with view := updateViewWithFunctorName e.view} - flatElabs.forM fun e => checkValidInductiveModifier e.view.modifiers elabFlatInductiveViews vars flatElabs discard <| flatElabs.mapM fun e => MetaM.run' do mkSumOfProducts e.view.declName elabCoinductive (flatElabs.map InductiveViewToCoinductiveElab) - elabInductiveViewsPostprocessingCoinductive (elabs.map (·.view)) else let res ← runTermElabM fun vars => do - elabs.forM fun e => checkValidInductiveModifier e.view.modifiers - checkNoInductiveNameConflicts elabs elabInductiveViews vars elabs - elabInductiveViewsPostprocessing (elabs.map (·.view)) res + elabInductiveViewsFinalize (elabs.map (·.view)) res + elabInductiveViewsPostprocessing (elabs.map (·.view)) def elabInductive (modifiers : Modifiers) (stx : Syntax) : CommandElabM Unit := do elabInductives #[(modifiers, stx)] diff --git a/tests/pkg/user_attr/UserAttr/BlaAttr.lean b/tests/pkg/user_attr/UserAttr/BlaAttr.lean index 907ec33bb6..880dea6a60 100644 --- a/tests/pkg/user_attr/UserAttr/BlaAttr.lean +++ b/tests/pkg/user_attr/UserAttr/BlaAttr.lean @@ -34,4 +34,32 @@ public meta initialize registerBuiltinAttribute { -- applicationTime := .afterCompilation } +syntax (name := myattr_beforeElaboration) "myattr_beforeElaboration" : attr +public meta initialize registerBuiltinAttribute { + name := `myattr_beforeElaboration + descr := "Simply traces when added, to debug application bugs" + add decl _ _ := do + let c := if (← getEnv).contains decl then m!"already in environment" else m!"not in environment" + logInfo m!"declaration `{decl}` tagged `myattr_beforeElaboration`, {c}" + applicationTime := .beforeElaboration +} +syntax (name := myattr_afterTypeChecking) "myattr_afterTypeChecking" : attr +public meta initialize registerBuiltinAttribute { + name := `myattr_afterTypeChecking + descr := "Simply traces when added, to debug application bugs" + add decl _ _ := do + let c := if (← getEnv).contains decl then m!"already in environment" else m!"not in environment" + logInfo m!"declaration `{decl}` tagged `myattr_afterTypeChecking`, {c}" + applicationTime := .afterTypeChecking +} +syntax (name := myattr_afterCompilation) "myattr_afterCompilation" : attr +public meta initialize registerBuiltinAttribute { + name := `myattr_afterCompilation + descr := "Simply traces when added, to debug application bugs" + add decl _ _ := do + let c := if (← getEnv).contains decl then m!"already in environment" else m!"not in environment" + logInfo m!"declaration `{decl}` tagged `myattr_afterCompilation`, {c}" + applicationTime := .afterCompilation +} + register_grind_attr my_grind diff --git a/tests/pkg/user_attr/UserAttr/Tst.lean b/tests/pkg/user_attr/UserAttr/Tst.lean index 219798ae28..9ee9ce32ca 100644 --- a/tests/pkg/user_attr/UserAttr/Tst.lean +++ b/tests/pkg/user_attr/UserAttr/Tst.lean @@ -225,3 +225,68 @@ example : boo (f (f (f x))) (f (f x)) = x := by end GrindAttr + + +namespace Issue13433 +/-! +Attributes with `beforeElaboration` were not being applied to `inductive` or `structure` commands +-/ + +/-- +info: declaration `Issue13433.A` tagged `myattr_beforeElaboration`, not in environment +--- +info: declaration `Issue13433.A` tagged `myattr_afterTypeChecking`, already in environment +--- +info: declaration `Issue13433.A` tagged `myattr_afterCompilation`, already in environment +-/ +#guard_msgs in +@[myattr_beforeElaboration, myattr_afterTypeChecking, myattr_afterCompilation] +structure A where +/-- +info: declaration `Issue13433.A` tagged `myattr_beforeElaboration`, already in environment +--- +info: declaration `Issue13433.A` tagged `myattr_afterTypeChecking`, already in environment +--- +info: declaration `Issue13433.A` tagged `myattr_afterCompilation`, already in environment +-/ +#guard_msgs in attribute [myattr_beforeElaboration, myattr_afterTypeChecking, myattr_afterCompilation] A + +/-- +info: declaration `Issue13433.B` tagged `myattr_beforeElaboration`, not in environment +--- +info: declaration `Issue13433.B` tagged `myattr_afterTypeChecking`, already in environment +--- +info: declaration `Issue13433.B` tagged `myattr_afterCompilation`, already in environment +-/ +#guard_msgs in +@[myattr_beforeElaboration, myattr_afterTypeChecking, myattr_afterCompilation] +inductive B where +/-- +info: declaration `Issue13433.B` tagged `myattr_beforeElaboration`, already in environment +--- +info: declaration `Issue13433.B` tagged `myattr_afterTypeChecking`, already in environment +--- +info: declaration `Issue13433.B` tagged `myattr_afterCompilation`, already in environment +-/ +#guard_msgs in attribute [myattr_beforeElaboration, myattr_afterTypeChecking, myattr_afterCompilation] B + +/-- +info: declaration `Issue13433.C` tagged `myattr_beforeElaboration`, not in environment +--- +info: declaration `Issue13433.C` tagged `myattr_afterTypeChecking`, already in environment +--- +info: declaration `Issue13433.C` tagged `myattr_afterCompilation`, already in environment +-/ +#guard_msgs in +@[myattr_beforeElaboration, myattr_afterTypeChecking, myattr_afterCompilation] +coinductive C : Prop where +/-- +info: declaration `Issue13433.C` tagged `myattr_beforeElaboration`, already in environment +--- +info: declaration `Issue13433.C` tagged `myattr_afterTypeChecking`, already in environment +--- +info: declaration `Issue13433.C` tagged `myattr_afterCompilation`, already in environment +-/ +#guard_msgs in attribute [myattr_beforeElaboration, myattr_afterTypeChecking, myattr_afterCompilation] C + +end Issue13433