ebd22c96ee
This PR ensures that failure in initial compilation marks the relevant definitions as `noncomputable`, inside and outside `noncomputable section`, so that follow-up errors/noncomputable markings are detected in initial compilation as well instead of somewhere down the pipeline. This may require additional `noncomputable` markers on definitions that depend on definitions inside `noncomputable section` but accidentally passed the new computability check. Reported at https://leanprover.zulipchat.com/#narrow/channel/270676-lean4/topic/Cryptic.20error.20message.20in.20new.20lean.20toolchain.3F.
16 lines
431 B
Text
16 lines
431 B
Text
module
|
|
|
|
meta import Module.Basic
|
|
|
|
/-! Basic phase restriction tests. -/
|
|
/--
|
|
error: Invalid definition `nonMeta`, may not access declaration `f` imported as `meta`; consider adding `import Module.Basic`
|
|
-/
|
|
#guard_msgs in
|
|
def nonMeta := f
|
|
|
|
/--
|
|
error: Invalid public `meta` definition `pubMetaImp`, `pubMeta` is not accessible here; consider adding `public import Module.Basic`
|
|
-/
|
|
#guard_msgs in
|
|
public meta def pubMetaImp := pubMeta
|