The Coq mailing list

[Pierre Courtieu <Pierre.Courtieu AT univ-orleans.fr>]

On 15 fév 2005, Yegor Bryukhov wrote:

>>> Hello,
>>> 
>>> I wonder if there are any built-in features for benchmarking.
>>> Specifically:
>>> 
>>> 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)?

>> Pierre Courtieu:

>> The command Time before another command or tactic lets you see the time
>> that the command took. 
>> 
>> Lemma ....
>> 
>> Time Auto.
>> ...
>> 
>> To have global time information on a file, I suppose the shell command
>> 'time' on the compilation command (coqc ...) is appropriate.

>Yegor Bryukhnov:

>but that would include not only proof checking time but 
>parsing/compilation itself.


Yes. If you want to know how much time a Save command takes: do 

Time Save.

instead of 

Save.

But of course this only works for one Save at a time.

Pierre


>>> 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?
>>> 
>
>> You can use the "Admitted." command, which stops a proof and put the
>> unfinished lemma as an axiom. 
>> 
>> Best regards,
>> 
>> Pierre
>