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?

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.

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:

Require Import ZArith.
Definition E := eq_refl 16%Z <: Zmod (1002 ^ 201) 17 = 16%Z.
$ \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

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?


Print Assumptions your_theorem. is usually reasonably fast

I was hoping to do this globally. I have many theorems :slight_smile:

1 Like

Looking at the code in, 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?

1 Like

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…

it certianly would help.

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

1 Like