coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- 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 measureInstead of "Qed" use "Time Qed".
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)?
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 notCoq is made to assure correctness of proofs, so you need to use some hack ...
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?
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/
- [Coq-Club] How to benchmark Coq, Yegor Bryukhov
- Re: [Coq-Club] How to benchmark Coq, Pierre Courtieu
- Message not available
- Message not available
- Re: [Coq-Club] How to benchmark Coq, Roland Zumkeller
- Re: [Coq-Club] How to benchmark Coq,
Yegor Bryukhov
- Re: [Coq-Club] How to benchmark Coq, Pierre Courtieu
- Re: [Coq-Club] How to benchmark Coq, jean-francois . monin
- Re: [Coq-Club] How to benchmark Coq,
Yegor Bryukhov
- Re: [Coq-Club] How to benchmark Coq, Roland Zumkeller
- Message not available
Archive powered by MhonArc 2.6.16.