From 0b93b3f1826cd8ab7cd61d8119854d32b59b54d6 Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Sun, 16 Nov 2025 21:34:23 +0100 Subject: [PATCH] chore: record uses of user-defined attributes as `shake` dependencies (#11202) --- src/Lean/Elab/Attributes.lean | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/src/Lean/Elab/Attributes.lean b/src/Lean/Elab/Attributes.lean index 29205a8149..aa0dd80523 100644 --- a/src/Lean/Elab/Attributes.lean +++ b/src/Lean/Elab/Attributes.lean @@ -7,6 +7,7 @@ module prelude public import Lean.Elab.Util +public import Lean.Compiler.InitAttr import Lean.Parser.Term public section @@ -56,6 +57,9 @@ def elabAttr [Monad m] [MonadEnv m] [MonadResolveName m] [MonadError m] [MonadMa | _ => throwErrorAt attr "Unknown attribute" 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 + 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`. -/ return { kind := attrKind, name := attrName, stx := attr }