[isabelle-dev] NEWS: Reactivated ML profiling

Makarius makarius at sketis.net
Wed Jun 9 14:01:42 CEST 2021

*** System ***

* ML profiling has been updated and reactivated, after some degration in

  - "isabelle build -o threads=1 -o profiling=..." works properly
    within the PIDE session context;

  - "isabelle profiling_report" now uses the session build database
    (like "isabelle log");

  - output uses non-intrusive tracing messages, instead of warnings.

This refers to Isabelle/014b944f4972.

For example:

isabelle build -o threads=1 -o profiling=time -c ZF
isabelle profiling_report ZF
isabelle profiling_report -c ZF

The threads=1 is required right now. A regular parallel session crashes like this:

  exception Fail raised (line 506 of "profiling.cpp"): Profiling is currently

(I need to ask David Matthews about it: a few years ago parallel profiling did
work to some extent.)


More information about the isabelle-dev mailing list