[isabelle-dev] Collecting statistics in Isabelle's kernel

[Makarius]

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 
lib/scripts/run-polyml).

So if you write your data at the start of Session.finish, it should 
normally work.  (The shutdown phase is a bit delicate.)


 	Makarius