quick build

Stream: general

[Reid Barton]

I forget whether this has been discussed before, but would it be possible to create a mode in which any lemma that would be proved in a side thread is instead just replaced by sorry?

[Reid Barton]

I know it's possible in principle for other stuff to examine these proofs, but hopefully (especially with the recent change involving irreducible) it doesn't actually happen...

[Reid Barton]

Ideally, one could parse and then discard the contents of all top-level lemmas for example.

[Gabriel Ebner]

Reid Barton said:

I forget whether this has been discussed before, but would it be possible to create a mode in which any lemma that would be proved in a side thread is instead just replaced by sorry?

Yes, it would be possible. Just put a mk_sorry in the right place. I tried this a few years (?) ago. It has some effect, but it's not an "espresso" build.

[Mario Carneiro]

Alternatively, it can thunk a proof and run it only if it is required, with the proof never being run if it is never used

[Reid Barton]

That would be ideal, yes. But the demand might only occur while compiling another module, so it sounds complicated, especially if you want to reuse the proof...