# Feature request: mode that disables Qed checking

**URL:** <https://discourse.rocq-prover.org/t/feature-request-mode-that-disables-qed-checking/279>\
**Category:** Using Rocq\
**Created:** [April 30, 2019, 10:00pm UTC](https://discourse.rocq-prover.org/t/feature-request-mode-that-disables-qed-checking/279 "2019-04-30T22:00:10Z")\
**Posts on this page:** 6\
**Page:** 1

<div class="post-metadata">

**Author:** ![tchajed](https://sea1.discourse-cdn.com/flex001/user_avatar/discourse.rocq-prover.org/tchajed/32/51_2.png) [@tchajed](https://discourse.rocq-prover.org/u/tchajed)\
**Post date:** [April 30, 2019, 10:00pm UTC](https://discourse.rocq-prover.org/t/feature-request-mode-that-disables-qed-checking/279/1 "2019-04-30T22:00:10Z")

</div>

Our development ([https://github.com/mit-pdos/armada](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.

---

<div class="post-metadata">

**Author:** ![ejgallego](https://sea1.discourse-cdn.com/flex001/user_avatar/discourse.rocq-prover.org/ejgallego/32/10_2.png) [@ejgallego](https://discourse.rocq-prover.org/u/ejgallego)\
**Post date:** [April 30, 2019, 11:29pm UTC](https://discourse.rocq-prover.org/t/feature-request-mode-that-disables-qed-checking/279/2 "2019-04-30T23:29:08Z")

</div>

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.

---

<div class="post-metadata">

**Author:** ![tchajed](https://sea1.discourse-cdn.com/flex001/user_avatar/discourse.rocq-prover.org/tchajed/32/51_2.png) [@tchajed](https://discourse.rocq-prover.org/u/tchajed)\
**Post date:** [May 1, 2019, 12:39am UTC](https://discourse.rocq-prover.org/t/feature-request-mode-that-disables-qed-checking/279/3 "2019-05-01T00:39:37Z")

</div>

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](https://github.com/coq/coq/issues/10036)) and get some guidance on implementing.

---

<div class="post-metadata">

**Author:** ![spitters](https://sea1.discourse-cdn.com/flex001/user_avatar/discourse.rocq-prover.org/spitters/32/125_2.png) [@spitters](https://discourse.rocq-prover.org/u/spitters)\
**Post date:** [May 1, 2019, 8:14am UTC](https://discourse.rocq-prover.org/t/feature-request-mode-that-disables-qed-checking/279/4 "2019-05-01T08:14:49Z")

</div>

This feature used to exist. I believe it was called qed\_nocheck .

---

<div class="post-metadata">

**Author:** ![ejgallego](https://sea1.discourse-cdn.com/flex001/user_avatar/discourse.rocq-prover.org/ejgallego/32/10_2.png) [@ejgallego](https://discourse.rocq-prover.org/u/ejgallego)\
**Post date:** [May 2, 2019, 12:08am UTC](https://discourse.rocq-prover.org/t/feature-request-mode-that-disables-qed-checking/279/5 "2019-05-02T00:08:02Z")

</div>

Interesting enough the current repository doesn’t show anything related to that @spitters, maybe we are talking about Coq pre-7.0 ?

---

<div class="post-metadata">

**Author:** ![spitters](https://sea1.discourse-cdn.com/flex001/user_avatar/discourse.rocq-prover.org/spitters/32/125_2.png) [@spitters](https://discourse.rocq-prover.org/u/spitters)\
**Post date:** [May 2, 2019, 8:15am UTC](https://discourse.rocq-prover.org/t/feature-request-mode-that-disables-qed-checking/279/6 "2019-05-02T08:15:19Z")

</div>

@herbelin should know.