Zulip Chat Archive

Stream: general

Topic: quick build


view this post on Zulip 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?

view this post on Zulip 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...

view this post on Zulip Reid Barton (May 14 2020 at 17:45):

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

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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