[isabelle-dev] NEWS: Timing dockable
makarius at sketis.net
Tue Mar 26 19:34:44 CET 2013
*** Prover IDE -- Isabelle/Scala/jEdit ***
* Dockable window "Timing" provides an overview of relevant command
This refers to Isabelle/625d2ec0bbff.
The dockable is still relatively basic, but might be useful to spot
performance bottlenecks in big developments. It has emerged now as one
more consequence of a lot of parallel performance measurements and that I
have done in the past couple of weeks (for papers, project presentations
etc.). I could need a really hot >= 16-core Xeon machine for testing ...
Here is an interesting thread on some French theorem prover mailing list
on the subject of multi-core execution:
I don't believe in any benefit of "competition", but Isabelle (with
Poly/ML) is presently roaring ahead. It has become difficult to find big
applications that take more than 1-2 min on 8 cores, but users will
undoubtably catch up again and burn more cycles, and hopefully do more
proofs with that.
More information about the isabelle-dev