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.
This PR adds documentation to builtin attributes like `@[refl]` or
`@[implemented_by]`.
Closes#8432
---------
Co-authored-by: David Thrane Christiansen <david@davidchristiansen.dk>
Co-authored-by: David Thrane Christiansen <david@lean-fro.org>
This PR fixes an issue where uses of 'noncomputable' definitions can get
incorrectly compiled, while also removing the use of 'noncomputable'
definitions altogether. Some uses of 'noncomputable' definitions (e.g.
Classical.propDecidable) do not get compiled correctly by type erasure.
Running the optimizer on the result can lead to them being optimized
away, eluding the later IR-level check for uses of noncomputable
definitions.
To fix this, we add a 'noncomputable' check earlier in the
erase_irrelevant pass.
