HomeIsabelle/Phabricator
Reactivated ML profiling

System

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

Isabelle2021:

  • 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
Written by makarius on Wed, Jun 9, 12:11 PM.
User
Projects
None
Subscribers
None

Event Timeline