Our development (https://github.com/mit-pdos/armada) takes 2,800 CPU seconds to compile, of which 930 are spent processing Qeds. During development, it would be really helpful to disable this checking; the continuous integration server could run them, or every so often we could check them to confirm the proofs are really working.
Could Coq add a flag that disables the re-checking of terms but still checks that there are no outstanding goals? Such a feature seems reasonably easy to implement and would give us a 33% improvement in build times for most purposes.
1 Like
Hi @tchajed, indeed that seems like a useful feature, I will support it myself in the new document manager.
I do think however that for these kind of requests, the issue tracker at github is better; if you post there I could provide some further guidance on how to implement it, basically you want to avoid calling add_constant with the term. [Note however that some stuff as section vars could interfere, so maybe you want to have a refined conditional on whether to call it]
I have a tree which provides a large cleanup on the proof save path, hopefully somebody would push it to Coq master soon as IMHO it would help a lot to implement your suggestion.
Awesome, thanks! I thought there might be some discussion so started here, but I’m happy to move to a GitHub issue (https://github.com/coq/coq/issues/10036) and get some guidance on implementing.
This feature used to exist. I believe it was called qed_nocheck .
Interesting enough the current repository doesn’t show anything related to that @spitters, maybe we are talking about Coq pre-7.0 ?