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

[Lars Noschinski]

Hi,

I'd like to use the current development version (for me currently
25d7b485df81) to collect some statistics in the kernel (in
bicompose_aux), preferably with a granularity on theory-level.
Currently, I do some aggregation of data in synchronized variables and
write it occasionally into some files.

However, I wonder whether there is some better way. AFAICS, 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?

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?

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?

[I should mention that this is just for debug purposes, with no
intention of pushing it into the main repository at some point]


  -- Lars