[isabelle-dev] NEWS: ML runtime statistics

Makarius makarius at sketis.net
Wed Jan 9 13:02:35 CET 2013

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

* Dockable window "Monitor" shows ML runtime statistics.

*** System ***

* Improved ML runtime statistics (heap, threads, future tasks etc.).

This refers to Isabelle/054f6bf349d2, with some further refinements later.

The main purpose is for system tools, usually based on Isabelle/Scala. 
Here is an example in Isabelle/15dc91cf4750 from today:

   $ isabelle build HOL-Auth
   $ isabelle scala
   scala> import isabelle._
   scala> val stats = ML_Statistics(Path.explode("$ISABELLE_OUTPUT/log/HOL-Auth.gz"))
   scala> stats.standard_frames

See also http://www.jfree.org/jfreechart for some standard functionaliy of 
these chart "frames" -- there is a right-click menu as well.

The implementation of standard_frames in src/Pure/ML/ml_statistics.scala
provides further clues how to work with the statistics programmatically.
This might be useful for isatest/mira at some point.


More information about the isabelle-dev mailing list