Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] How to benchmark Coq

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] How to benchmark Coq


chronological Thread 
  • From: Roland Zumkeller <Roland.Zumkeller AT polytechnique.fr>
  • To: Yegor Bryukhov <ybryukhov AT gc.cuny.edu>
  • Cc: coq-club AT pauillac.inria.fr
  • Subject: Re: [Coq-Club] How to benchmark Coq
  • Date: Wed, 16 Feb 2005 19:19:18 +0100
  • List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>

(looks like we forgot to cc the list - citations are below)

As Jean-Christophe Filliâtre suggested in a recent post, proof terms constructed by a script are rechecked by the "Save" command. Still it seems that "Save" cleverly reuses some of the judgements that have already been obtained from the kernel by the script (thus obscuring the total checking time), as shown by this example:
  Variable P : nat -> Prop.
  Hypothesis H : P (500*100 - 500*100).

  Lemma P_0 : P 0.
  exact H. (* takes a long time *)
  Save. (* takes little time *)

What time do you want to measure? Proof search, or just checking of already constructed proofs?
In the latter case you could display the proof term with the "Print" command, then recheck its coercion to the goal:
  Check H : P 0.

Hope this helps.

Thank you very much, Roland.
Your trick with inconsistent assumption was helpful.

Unfortunately Time Qed works only for individual proofs.
It seems that measuring "Load" or compilations time is closer to what I need.
Ideally, I'd prefer to load compiled script and replay proofs stored there (to exclude parsing and compilation time) but it seems impossible in Coq.


Roland Zumkeller wrote:
1. I have bunch of lemmas with proofs and I want to measure
how much time it will take to check those proofs. May I ask Coq to
measure it or I have to use external tools (like watches on my wrist)?
Instead of "Qed" use "Time Qed".
This will give you the time coq spent checking the proof term developed by your script (not the execution time of your proof script).
2. Again I have a bunch of lemmas with proofs but some of them are not
correct (simply because some decision procedure didn't succeed).
CoqIDE stops on such lemma and dos not allow to proceed to the next
statement. May I force Coq to check several proofs and not to stop on
the first failure?
Coq is made to assure correctness of proofs, so you need to use some hack ...
You could make an inconsistent assumption
  Hypothesis admit : forall A:Type, A.
and use it to cheat everytime your decision procedure fails
  Lemma l1 : 2=3.
  auto ||
  apply admit.
  Time Qed.
Replace "auto" by your decision procedure - if it succeeds, "apply admit" will not get called. If the procedure fails "apply admit" is used to cheat and have Coq process the rest of the file.
(The command "Admitted" doesn't work here since we would have to know a priori if the proof worked or no every time).
Regards,
Roland
--
http://www.lix.polytechnique.fr/~zumkeller/


--
Best regards,
Yegor
__________________________________________________________
Yegor Bryukhov, PhD student at GC CUNY
office:       4330
office phone: +1(212)817-8653
cell phone:   +1(917)650-2035
e-mail:       
ybryukhov AT gc.cuny.edu
 
ynb AT mail.ru
home-page:    http://www.cs.gc.cuny.edu/~yegor/





Archive powered by MhonArc 2.6.16.

Top of Page