Stream: general

Topic: quick build

Reid Barton (May 14 2020 at 17:39):

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 (May 14 2020 at 17:44):

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 (May 14 2020 at 17:45):

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

Gabriel Ebner (May 14 2020 at 17:49):

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 (May 14 2020 at 18:59):

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 (May 14 2020 at 19:01):

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...

Last updated: May 15 2021 at 23:13 UTC