coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: jean-francois.monin AT imag.fr
- To: Roland Zumkeller <Roland.Zumkeller AT polytechnique.fr>
- Cc: Yegor Bryukhov <ybryukhov AT gc.cuny.edu>, coq-club AT pauillac.inria.fr
- Subject: Re: [Coq-Club] How to benchmark Coq
- Date: Wed, 16 Feb 2005 20:05:51 +0100
- List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>
Roland Zumkeller a ecrit :
> (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 *)
The difference is not that big : Time Save takes yields about 1/2 of
Time Exact (measured with larger values than 500*100).
In the case of this lemma, the difference comes probably from
the reduction algorithm in use.
Jean-Francois
--
Jean-François Monin
VERIMAG - Centre Equation http://www-verimag.imag.fr/~monin/
2 avenue de Vignate tel (+33 | 0) 4 56 52 03 72
F-38610 GIERES fax (+33 | 0) 4 56 52 03 44
- [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.