e6dfdfdcee
This PR makes the elaborator reject `@[foo]` when the module that registers `foo` is not visibly imported into the current file but merely loaded as IR. Previously such uses silently elaborated but led to divergence of cmdline and server behavior and caused `lake shake --fix` to flip-flop on successive runs (#13599).
20 lines
724 B
Text
20 lines
724 B
Text
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 loaded for IR only (reached as a private `meta` dependency). Add an import of `UserAttr.BlaAttr`.
|
|
-/
|
|
#guard_msgs in
|
|
@[my_simp]
|
|
theorem midVal_eq : midVal = 17 := rfl
|
|
|
|
end
|