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).
13 lines
292 B
Text
13 lines
292 B
Text
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
|