[isabelle-dev] NEWS: Timing dockable

[Makarius]

*** Prover IDE -- Isabelle/Scala/jEdit ***

* Dockable window "Timing" provides an overview of relevant command
timing information.

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: 
https://sympa.inria.fr/sympa/arc/coq-club/2013-03/msg00033.html

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.


 	Makarius