# Coqchk

**URL:** <https://discourse.rocq-prover.org/t/coqchk/1047>\
**Category:** Using Rocq\
**Created:** [September 9, 2020, 8:34pm UTC](https://discourse.rocq-prover.org/t/coqchk/1047 "2020-09-09T20:34:48Z")\
**Posts on this page:** 10\
**Page:** 1

<div class="post-metadata">

**Author:** ![vzaliva](https://sea1.discourse-cdn.com/flex001/user_avatar/discourse.rocq-prover.org/vzaliva/32/72_2.png) [@vzaliva](https://discourse.rocq-prover.org/u/vzaliva)\
**Post date:** [September 9, 2020, 8:34pm UTC](https://discourse.rocq-prover.org/t/coqchk/1047/1 "2020-09-09T20:34:48Z")

</div>

I have a sizeable Coq project of about 50Kloc. It takes about 30 min to compile. Recently I tried to run `coqchk` on it using the `validate` target generated by `coq_makefile`. It has been running for 4 hours and has not yet finished.

Is it normal for it to take so long? Why this process is longer than the actual compilation?

---

<div class="post-metadata">

**Author:** ![Blaisorblade](https://sea1.discourse-cdn.com/flex001/user_avatar/discourse.rocq-prover.org/blaisorblade/32/56_2.png) [@Blaisorblade](https://discourse.rocq-prover.org/u/Blaisorblade)\
**Post date:** [September 10, 2020, 8:01am UTC](https://discourse.rocq-prover.org/t/coqchk/1047/2 "2020-09-10T08:01:34Z")

</div>

TLDR Yes it’s slow, even on smaller projects, and it’s not actually guaranteed to succeed even on correct proofs (because of issues; that’s tracked on github, no insight here). You can try running coqchk on smaller files to see how long it takes there.

I’ll leave the why to others.

---

<div class="post-metadata">

**Author:** ![silene](https://sea1.discourse-cdn.com/flex001/user_avatar/discourse.rocq-prover.org/silene/32/485_2.png) [@silene](https://discourse.rocq-prover.org/u/silene)\
**Post date:** [September 10, 2020, 1:34pm UTC](https://discourse.rocq-prover.org/t/coqchk/1047/3 "2020-09-10T13:34:51Z")

</div>

> [@vzaliva](#):
>
> Why this process is longer than the actual compilation?

If your development depends on the speed of the reduction engine, you should keep in mind that `coqchk` only uses the `lazy` one. Here is a small example:

```coq
Require Import ZArith.
Definition E := eq_refl 16%Z <: Zmod (1002 ^ 201) 17 = 16%Z.

```

```console
$ \time coqc a.v
0.29user 0.06system 0:00.35elapsed 99%CPU (0avgtext+0avgdata 327532maxresident)k
0inputs+120outputs (0major+78494minor)pagefaults 0swaps
$ \time coqchk -admit Coq.ZArith.ZArith a.vo
...
Checking library: a
  checking cst:a.E
Modules were successfully checked
...
6.32user 0.06system 0:06.39elapsed 99%CPU (0avgtext+0avgdata 180876maxresident)k
0inputs+0outputs (0major+44549minor)pagefaults 0swaps

```

---

<div class="post-metadata">

**Author:** ![vzaliva](https://sea1.discourse-cdn.com/flex001/user_avatar/discourse.rocq-prover.org/vzaliva/32/72_2.png) [@vzaliva](https://discourse.rocq-prover.org/u/vzaliva)\
**Post date:** [September 10, 2020, 3:47pm UTC](https://discourse.rocq-prover.org/t/coqchk/1047/4 "2020-09-10T15:47:13Z")

</div>

Thanks! So basically it is not very useful right now. At least for me. It have been running for 24 hours now…

I want to check what are the axioms my project relies upon. If there is an easy way to do this?

Vadim

---

<div class="post-metadata">

**Author:** ![cpitclaudel](https://sea1.discourse-cdn.com/flex001/user_avatar/discourse.rocq-prover.org/cpitclaudel/32/337_2.png) [@cpitclaudel](https://discourse.rocq-prover.org/u/cpitclaudel)\
**Post date:** [September 10, 2020, 4:22pm UTC](https://discourse.rocq-prover.org/t/coqchk/1047/5 "2020-09-10T16:22:58Z")

</div>

`Print Assumptions your_theorem.` is usually reasonably fast

---

<div class="post-metadata">

**Author:** ![vzaliva](https://sea1.discourse-cdn.com/flex001/user_avatar/discourse.rocq-prover.org/vzaliva/32/72_2.png) [@vzaliva](https://discourse.rocq-prover.org/u/vzaliva)\
**Post date:** [September 10, 2020, 4:24pm UTC](https://discourse.rocq-prover.org/t/coqchk/1047/6 "2020-09-10T16:24:22Z")

</div>

I was hoping to do this globally. I have many theorems 🙂

---

<div class="post-metadata">

**Author:** ![cpitclaudel](https://sea1.discourse-cdn.com/flex001/user_avatar/discourse.rocq-prover.org/cpitclaudel/32/337_2.png) [@cpitclaudel](https://discourse.rocq-prover.org/u/cpitclaudel)\
**Post date:** [September 10, 2020, 6:52pm UTC](https://discourse.rocq-prover.org/t/coqchk/1047/7 "2020-09-10T18:52:14Z")

</div>

Looking at the code in assumptions.ml, it looks like it wouldn’t be too hard to allow `Print Assumptions` to run on a complete module instead of a single term. Would that help?

---

<div class="post-metadata">

**Author:** ![Blaisorblade](https://sea1.discourse-cdn.com/flex001/user_avatar/discourse.rocq-prover.org/blaisorblade/32/56_2.png) [@Blaisorblade](https://discourse.rocq-prover.org/u/Blaisorblade)\
**Post date:** [September 10, 2020, 7:30pm UTC](https://discourse.rocq-prover.org/t/coqchk/1047/8 "2020-09-10T19:30:29Z")

</div>

FWIW, my testcases use `Print Assumptions` on the 5 top-level theorems I’d mention in my CS paper. But I can see how that won’t scale to the 500 theorems of a math paper…

---

<div class="post-metadata">

**Author:** ![vzaliva](https://sea1.discourse-cdn.com/flex001/user_avatar/discourse.rocq-prover.org/vzaliva/32/72_2.png) [@vzaliva](https://discourse.rocq-prover.org/u/vzaliva)\
**Post date:** [September 10, 2020, 9:12pm UTC](https://discourse.rocq-prover.org/t/coqchk/1047/9 "2020-09-10T21:12:00Z")

</div>

it certianly would help.

---

<div class="post-metadata">

**Author:** ![cpitclaudel](https://sea1.discourse-cdn.com/flex001/user_avatar/discourse.rocq-prover.org/cpitclaudel/32/337_2.png) [@cpitclaudel](https://discourse.rocq-prover.org/u/cpitclaudel)\
**Post date:** [September 10, 2020, 9:38pm UTC](https://discourse.rocq-prover.org/t/coqchk/1047/10 "2020-09-10T21:38:08Z")

</div>

Do you want to open a feature request on the tracker? I think it would be a nice feature to have.