Coqchk

Using Coq
1

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?

2

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.

3

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
4

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

5

Print Assumptions your_theorem. is usually reasonably fast

6

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

1 Like
7

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?

1 Like
8

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…

9

it certianly would help.

10

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

1 Like