[isabelle-dev] Collecting statistics in Isabelle's kernel
makarius at sketis.net
Wed Feb 19 21:25:52 CET 2014
On Wed, 19 Feb 2014, Lars Noschinski wrote:
> I do some aggregation of data in synchronized variables and write it
> occasionally into some files.
Synchronized variables are fine to collect global information. Normally I
would write the result out only in the very end, either in a specific
file, or via "broadcast" into the log file.
> I can get a global theory context from the theorem passed into
> bicompose_aux (as done for the trace_unify_failure flag) -- I assume I
> cannot use this context to store my data?
A theory is not a proper context, and is rarely usable to maintain any
data during inferencing. In ancient times we occasionally had some
(unsynchronized) refs in theories for that purpose, but a global
Synchronized.var is better.
> As for writing data into files, it might be easier to pass structured
> data into Isabelle/Scala. Can I do this when using Build.build, as
> Makarius suggested some time ago?
Build does this to a very limited extent at the moment, e.g. some inline
YXML trees that are later fished from the log files (command timing).
> A last question: I do some basic aggregation of the data before pushing
> it out. To avoid losing data, I need to do a final push when the build
> (or maybe a theory) finishes. Is there some point in the build process
> where I can easily hook in to achieve that?
Session.finish() is basically the last thing that happens, just before the
end of Build.build, and the implicit commit() of the heap image (see
So if you write your data at the start of Session.finish, it should
normally work. (The shutdown phase is a bit delicate.)
More information about the isabelle-dev