From 899fcc6d7e7df2b604d789d11d9cb46219edbebb Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Sat, 2 May 2026 13:27:23 +0000 Subject: [PATCH 1/2] fix: reject attribute uses whose home module is reached only as `meta` This PR makes the elaborator reject `@[foo]` when the module that registers `foo` is reachable only via a `meta import` chain, with an error pointing at the missing non-`meta` `import`. Previously such uses silently elaborated but caused `shake --fix` to flip-flop on successive runs (issue #13599) because the missing `metaExt` left an attribute's recorded import stuck as `meta`. The check fires only for `regular_initialize`-registered attributes (i.e. user-defined ones, not `builtin_initialize` core attributes) whose home module has `irPhases == .comptime`. --- src/Lean/Elab/Attributes.lean | 11 +++++++++++ tests/pkg/user_attr/UserAttr.lean | 1 + tests/pkg/user_attr/UserAttr/MetaMid.lean | 13 +++++++++++++ tests/pkg/user_attr/UserAttr/MetaUser.lean | 20 ++++++++++++++++++++ 4 files changed, 45 insertions(+) create mode 100644 tests/pkg/user_attr/UserAttr/MetaMid.lean create mode 100644 tests/pkg/user_attr/UserAttr/MetaUser.lean diff --git a/src/Lean/Elab/Attributes.lean b/src/Lean/Elab/Attributes.lean index dae6c6fc3e2e..6c6be56136ed 100644 --- a/src/Lean/Elab/Attributes.lean +++ b/src/Lean/Elab/Attributes.lean @@ -63,6 +63,17 @@ def elabAttr [Monad m] [MonadEnv m] [MonadResolveName m] [MonadError m] [MonadMa | throwError "Unknown attribute `[{attrName}]`" if let .ok impl := getAttributeImpl (← getEnv) attrName then if regularInitAttr.getParam? (← getEnv) impl.ref |>.isSome then -- skip `builtin_initialize` attributes + -- Reject attribute uses where the implementation's home module has been reached only as a + -- `meta` dep (`irPhases == .comptime`). In that case `metaExt` may not be visible — even if + -- the module's own data was loaded (e.g. directly meta-imported), reachable transitive + -- modules with `import` from a meta-imported parent are loaded IR-only. Forcing a non-meta + -- import keeps shake's recording stable (issue #13599). + if let some idx := (← getEnv).getModuleIdxFor? impl.ref then + let env ← getEnv + if env.header.modules[idx]?.any (·.irPhases == .comptime) then + let modName := env.header.modules[idx]!.module + throwError m!"Cannot use attribute `[{attrName}]`: module `{modName}` is reached only \ + as a `meta` dependency. Add a non-`meta` `import {modName}`." 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`. -/ diff --git a/tests/pkg/user_attr/UserAttr.lean b/tests/pkg/user_attr/UserAttr.lean index ec633fea1cf1..24e108990f72 100644 --- a/tests/pkg/user_attr/UserAttr.lean +++ b/tests/pkg/user_attr/UserAttr.lean @@ -1,4 +1,5 @@ import UserAttr.Tst +import UserAttr.MetaUser open Lean diff --git a/tests/pkg/user_attr/UserAttr/MetaMid.lean b/tests/pkg/user_attr/UserAttr/MetaMid.lean new file mode 100644 index 000000000000..fd8303405fbc --- /dev/null +++ b/tests/pkg/user_attr/UserAttr/MetaMid.lean @@ -0,0 +1,13 @@ +module + +import UserAttr.BlaAttr + +/-! Middle module that plain-imports `UserAttr.BlaAttr`, used by `UserAttr.MetaUser` to set up the +`meta import` chain that triggers the regression in +https://github.com/leanprover/lean4/issues/13599. -/ + +@[expose] public section + +def midVal : Nat := 17 + +end diff --git a/tests/pkg/user_attr/UserAttr/MetaUser.lean b/tests/pkg/user_attr/UserAttr/MetaUser.lean new file mode 100644 index 000000000000..79622b4d454c --- /dev/null +++ b/tests/pkg/user_attr/UserAttr/MetaUser.lean @@ -0,0 +1,20 @@ +module + +public meta import UserAttr.MetaMid +meta import Lean.Elab.GuardMsgs + +/-! Regression test for https://github.com/leanprover/lean4/issues/13599: using `@[my_simp]` (an +attribute registered in `UserAttr.BlaAttr`) while reaching `BlaAttr` only via a `meta import` +chain (`UserAttr.MetaMid → import UserAttr.BlaAttr`) used to make `shake --fix` flip-flop. The +elaborator now rejects such uses with a clear error pointing at the missing import. -/ + +@[expose] public section + +/-- +error: Cannot use attribute `[my_simp]`: module `UserAttr.BlaAttr` is reached only as a `meta` dependency. Add a non-`meta` `import UserAttr.BlaAttr`. +-/ +#guard_msgs in +@[my_simp] +theorem midVal_eq : midVal = 17 := rfl + +end From 5a6a34903385765bd5d18503dcfe38ef724c6b55 Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Sun, 3 May 2026 10:33:47 +0000 Subject: [PATCH 2/2] less restrictive check --- src/Lean/Elab/Attributes.lean | 15 +++++++-------- src/Lean/Environment.lean | 16 ++++++++-------- tests/pkg/user_attr/UserAttr/MetaUser.lean | 2 +- 3 files changed, 16 insertions(+), 17 deletions(-) diff --git a/src/Lean/Elab/Attributes.lean b/src/Lean/Elab/Attributes.lean index 6c6be56136ed..fe3fd8eae882 100644 --- a/src/Lean/Elab/Attributes.lean +++ b/src/Lean/Elab/Attributes.lean @@ -63,17 +63,16 @@ def elabAttr [Monad m] [MonadEnv m] [MonadResolveName m] [MonadError m] [MonadMa | throwError "Unknown attribute `[{attrName}]`" if let .ok impl := getAttributeImpl (← getEnv) attrName then if regularInitAttr.getParam? (← getEnv) impl.ref |>.isSome then -- skip `builtin_initialize` attributes - -- Reject attribute uses where the implementation's home module has been reached only as a - -- `meta` dep (`irPhases == .comptime`). In that case `metaExt` may not be visible — even if - -- the module's own data was loaded (e.g. directly meta-imported), reachable transitive - -- modules with `import` from a meta-imported parent are loaded IR-only. Forcing a non-meta - -- import keeps shake's recording stable (issue #13599). + -- Reject attribute uses where the implementation's home module has been loaded for IR only: + -- in that case `metaExt` is missing and shake's `recordExtraModUseFromDecl` would record a + -- stale `isMeta` flag (issue #13599). Force the user to import the module as a regular dep. if let some idx := (← getEnv).getModuleIdxFor? impl.ref then let env ← getEnv - if env.header.modules[idx]?.any (·.irPhases == .comptime) then + if env.header.modules[idx]?.any (!·.hasData) then let modName := env.header.modules[idx]!.module - throwError m!"Cannot use attribute `[{attrName}]`: module `{modName}` is reached only \ - as a `meta` dependency. Add a non-`meta` `import {modName}`." + throwError m!"Cannot use attribute `[{attrName}]`: module `{modName}` is loaded for IR \ + only (reached as a private `meta` dependency). Add a non-private import \ + of `{modName}`." 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`. -/ diff --git a/src/Lean/Environment.lean b/src/Lean/Environment.lean index 9bd043e8ff97..7b5721899bc2 100644 --- a/src/Lean/Environment.lean +++ b/src/Lean/Environment.lean @@ -147,6 +147,8 @@ structure ModuleData where structure EffectiveImport extends Import where /-- Phases for which the import's IR is available. -/ irPhases : IRPhases + /-- Whether the import's `.olean*` data has been loaded (otherwise only the `.ir` is). -/ + hasData : Bool deriving Inhabited /-- Environment fields that are not used often. -/ @@ -1980,14 +1982,12 @@ private structure ImportedModule extends EffectiveImport where parts : Array (ModuleData × CompactedRegion) /-- `.ir` data, if loaded. -/ irData? : Option (ModuleData × CompactedRegion) - /-- If true, `.olean*` data should be imported. -/ - needsData : Bool /-- If true, IR is loaded transitively. -/ needsIRTrans : Bool /-- The main module data that will eventually be used to construct the publicly accessible constants. -/ private def ImportedModule.publicModule? (self : ImportedModule) : Option ModuleData := do - if self.needsData then + if self.hasData then self.parts[0]?.map (·.1) else -- (should not have any constants) @@ -2000,7 +2000,7 @@ private def ImportedModule.getData? (self : ImportedModule) (level : OLeanLevel) /-- The main module data that will eventually be used to construct the kernel environment. -/ private def ImportedModule.mainModule? (self : ImportedModule) : Option ModuleData := - if self.needsData then + if self.hasData then self.getData? (if self.importAll then .private else .exported) else self.irData?.map (·.1) @@ -2150,16 +2150,16 @@ where -- when module is already imported, bump flags let importAll := importAll || mod.importAll let isExported := isExported || mod.isExported - let needsData := needsData || mod.needsData + let needsData := needsData || mod.hasData let needsIRTrans := needsIRTrans || mod.needsIRTrans let needsIR := needsIRTrans || importAll let irPhases := if irPhases == mod.irPhases then irPhases else .all let parts ← if needsData && mod.parts.isEmpty then loadData i else pure mod.parts let irData? ← if needsIR && mod.irData?.isNone then loadIR? i else pure mod.irData? if importAll != mod.importAll || isExported != mod.isExported || - needsIRTrans != mod.needsIRTrans || needsData != mod.needsData || irPhases != mod.irPhases then + needsIRTrans != mod.needsIRTrans || needsData != mod.hasData || irPhases != mod.irPhases then modify fun s => { s with moduleNameMap := s.moduleNameMap.insert i.module { mod with - importAll, isExported, irPhases, parts, irData?, needsData, needsIRTrans }} + importAll, isExported, irPhases, parts, irData?, hasData := needsData, needsIRTrans }} -- bump entire closure goRec mod continue @@ -2167,7 +2167,7 @@ where -- newly discovered module let parts ← if needsData then loadData i else pure #[] let irData? ← if needsIR then loadIR? i else pure none - let mod := { i with importAll, isExported, irPhases, parts, irData?, needsIRTrans, needsData } + let mod := { i with importAll, isExported, irPhases, parts, irData?, needsIRTrans, hasData := needsData } goRec mod modify fun s => { s with moduleNameMap := s.moduleNameMap.insert i.module mod diff --git a/tests/pkg/user_attr/UserAttr/MetaUser.lean b/tests/pkg/user_attr/UserAttr/MetaUser.lean index 79622b4d454c..acb9760014a7 100644 --- a/tests/pkg/user_attr/UserAttr/MetaUser.lean +++ b/tests/pkg/user_attr/UserAttr/MetaUser.lean @@ -11,7 +11,7 @@ elaborator now rejects such uses with a clear error pointing at the missing impo @[expose] public section /-- -error: Cannot use attribute `[my_simp]`: module `UserAttr.BlaAttr` is reached only as a `meta` dependency. Add a non-`meta` `import UserAttr.BlaAttr`. +error: Cannot use attribute `[my_simp]`: module `UserAttr.BlaAttr` is loaded for IR only (reached as a private `meta` dependency). Add a non-private import of `UserAttr.BlaAttr`. -/ #guard_msgs in @[my_simp]