[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.
Makarius
More information about the isabelle-dev
mailing list