From e97c1505f05f12fefde0590106ab7e8241743a75 Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Thu, 20 Nov 2025 21:39:27 +0100 Subject: [PATCH] fix: shake: register attribute rev use independent of `initialize` kind (#11293) --- src/Lean/Elab/Attributes.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Lean/Elab/Attributes.lean b/src/Lean/Elab/Attributes.lean index aa0dd80523..29f3cba23f 100644 --- a/src/Lean/Elab/Attributes.lean +++ b/src/Lean/Elab/Attributes.lean @@ -58,7 +58,7 @@ def elabAttr [Monad m] [MonadEnv m] [MonadResolveName m] [MonadError m] [MonadMa let .ok _impl := getAttributeImpl (← getEnv) attrName | throwError "Unknown attribute `[{attrName}]`" if let .ok impl := getAttributeImpl (← getEnv) attrName then - if isIOUnitRegularInitFn (← getEnv) impl.ref then -- skip `builtin_initialize` attributes + if regularInitAttr.getParam? (← getEnv) impl.ref |>.isSome then -- skip `builtin_initialize` attributes recordExtraModUseFromDecl (isMeta := true) impl.ref /- The `AttrM` does not have sufficient information for expanding macros in `args`. So, we expand them before here before we invoke the attributer handlers implemented using `AttrM`. -/