From 7ef229d03d936db2b71629ade1fb2e9cbbc0b95d Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Thu, 20 Nov 2025 16:39:38 +0100 Subject: [PATCH] chore: shake: re-add `attribute` rev use (#11288) Global `attribute` commands on non-local declarations are impossible to track granularly a priori and so should be preserved by `shake` by default. A new `shake` option could be added to ignore these dependencies for evaluation. --- src/Lean/Elab/Declaration.lean | 5 +++++ tests/lean/run/extraModUses.lean | 2 +- 2 files changed, 6 insertions(+), 1 deletion(-) diff --git a/src/Lean/Elab/Declaration.lean b/src/Lean/Elab/Declaration.lean index a09ded8a30..7f20864852 100644 --- a/src/Lean/Elab/Declaration.lean +++ b/src/Lean/Elab/Declaration.lean @@ -330,6 +330,11 @@ def elabMutual : CommandElab := fun stx => do Term.applyAttributes declName attrs for attrName in toErase do Attribute.erase declName attrName + if (← getEnv).isImportedConst declName && attrs.any (·.kind == .global) then + -- If an imported declaration is marked with a global attribute, there is no good way to track + -- its use generally and so Shake should conservatively preserve imports of the current + -- module. + recordExtraRevUseOfCurrentModule @[builtin_command_elab Lean.Parser.Command.«initialize»] def elabInitialize : CommandElab | stx@`($declModifiers:declModifiers $kw:initializeKeyword $[$id? : $type? ←]? $doSeq) => do diff --git a/tests/lean/run/extraModUses.lean b/tests/lean/run/extraModUses.lean index 908747de0e..eb2a53e4b7 100644 --- a/tests/lean/run/extraModUses.lean +++ b/tests/lean/run/extraModUses.lean @@ -174,7 +174,7 @@ attribute [grind =] List.append /-- info: Entries: [import Init.Grind.Attr, public import Init.Prelude] -Is rev mod use: false +Is rev mod use: true -/ #guard_msgs in #eval showExtraModUses