RFC: built in option to suppress compilation of defs

[mattrobball]

Proposal

Add a built in option to disable compilation. Here is one possibility. (Edit: this is too naive.)

• User Experience: Currently, Lean attempts to compile declarations in noncomputable section's by default. If an error is thrown, then compilation is not required and Lean proceeds. There are large unexpected spikes in compilation Spikes in compilation + maximum resident set size leanprover-community/mathlib4#7103 that can occur, especially when the underlying code becomes more efficient to build. Additionally, some modules are not meant for compilation. With the current design, those modules have to mark each declaration noncomputable to avoid the time spent on compilation. This is tedious.

• Beneficiaries: Until the costs, in terms of compilation, of the current design are more predictable, every user benefits. Users interested in purely mathematical constructions will be able to significantly speed up their workflow.

• Maintainability: Option bloat is bad. But I think the benefits to users outweighs the cost here.

Community Feedback

Ideas should be discussed on the Lean Zulip prior to submitting a proposal. Summarize all prior discussions and link them here.

We have had multiple discussions about the spikes in the compilation. One of the most recent is here. The main focus there is parsing declarations to attach the noncomputable one by one via automation. However, syntax is very diverse so a broad solution is tricky to implement.

Impact

Add 👍 to issues you consider important. If others benefit from the changes in this proposal being added, please ask them to add 👍 to it.

[sgouezel]

A version of this has been implemented in mathlib, with the very hackish supress_compilation tactic (https://github.com/leanprover-community/mathlib4/blob/master/Mathlib/Tactic/SuppressCompilation.lean)