max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

fix: shake: register attribute rev use independent of initialize kind (#11293)

Browse source
This commit is contained in:
Sebastian Ullrich 2025-11-20 21:39:27 +01:00 • committed by GitHub
parent b6399e18c3
commit e97c1505f0
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
1 changed files with 1 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/Lean/Elab/Attributes.lean
View file

@ -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`. -/