[RFC] optional smaller olean files

[fpvandoorn]

Description

There are two big contributors to the olean sizes for Mathlib4 with only minimal value:

• proofs of theorems
• compilation of "mathematical" definitions

These two pieces of data are used only rarely by Mathlib4 contributors, and I think it would be nice if we have the option to get olean files without these two components.

Proposal

Add a flag that makes Lean produce .olean files without these two components. More precisely, with this flag:

• Lean doesn't store the proof of theorems (and the value of propositional definitions) in the olean file. It still checks the theorems and errors if the proof is wrong.
• Lean doesn't store the intermediate representation/c-code for mathematical definitions. As a proxy for "what is a mathematical definition" we could use "does this definition occur in a noncomputable section. We still need the ability to make certain definitions computable (e.g. delaborators), perhaps using a new computable keyword.

Moreover, Lean should be able to import such .olean files (even with this flag enabled). Perhaps there should also be a flag that forces oleans of imported files to be complete (including the two pieces of data above).

Consequences

Positive: This option would reduce .olean file size by roughly 2x (in the linked Zulip thread below Mario computes that there is a 31% reduction without proofs. On a small sample of Mathlib files, the environment extensions with the intermediate representations / compiler are some of the largest environment extensions.
I expect that Mathlib4 users will have the ability to download both the partial and full .olean caches, depending on whether they want all the information.

Negative As far as I can tell, with the partial olean files you can do everything, except the following:

1. Cannot #print the value on a theorem in an imported file
2. Cannot run #print axioms on a theorem
3. Cannot #eval mathematical definitions.

Most of the time, Mathlib users don't run any of these commands. If they do want this, they can easily get the full .olean caches.

Zulip discussion