The Coq mailing list

[Yegor Bryukhov <ybryukhov AT gc.cuny.edu>]

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)?

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?

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/