The Coq mailing list

[Tej Chajed <tchajed AT mit.edu>]

I would second using vos and vok to speed up your development workflow.

Along the same lines we unsoundly skip Qeds during CI but check them locally. Unfortunately Coq doesn't have a native way to do this (see https://github.com/coq/coq/issues/10036), but you can basically implement the feature with sed: https://github.com/mit-pdos/perennial/blob/master/etc/disable-qed.sh (this is really a shameless plug for this hack, and a plea to get #10036 implemented so we don't need a hack).

At least in our development Qeds take about 20% of the compilation time so this is a pretty big performance improvement for a single change. I also think it's quite safe since I haven't seen a failure at Qed time in a long time, and never since I started using Iris. If you do a lot of computation in a proof that might not be the case (you might have horrible performance at Qed time that needs to be fixed eventually), or if you use fancy universe features like universe polymorphism (you'll be more likely to run into bugs that only show up at Qed time).

On Fri, Apr 2, 2021 at 2:11 PM Pierre Courtieu <pierre.courtieu AT gmail.com> wrote:

Hi

I think this feature disappeared at some point. But you can reduce
drastically your waiting time by building ".vos" instead of ".vo".
Unsound but extremely fast.

My mojo:
1) add "Proof using ..." annotations everywhere in your sections,
otherwise the compilation time will not decrease. There is a mode in
proofgeneral where these annotations are added automatically when you
pass a Qed.
2) compile .vok from time to time to check proofs.
3) compile .vo file to really check universe constraints once a day
(or week maybe if you don't expect such problems).
Best
Pierre

Le ven. 2 avr. 2021 à 19:27, Abhishek Anand
<abhishek.anand.iitg AT gmail.com> a écrit :
>
> Very often, I have a file X.v which I know has errors.
> So to fix them, I can only edit it interactively, e.g. in emacs/company-coq
> When the fixing is done and the whole buffer has been processed by coq, can I ask the editor/coqtop to dump a .vo file for the current .v file?
> Otherwise, I have to reprocess the whole file by coqc outside the editor which can take many minutes.
>
>
> -- Abhishek
> http://www.cs.cornell.edu/~aa755/