Email Gateway (Jun 09 2021 at 12:01): Email Gateway (Jun 09 2021 at 12:01):From: Makarius <makarius@sketis.net>
* 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
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
active
(I need to ask David Matthews about it: a few years ago parallel profiling did
work to some extent.)
Makarius
isabelle-dev mailing list
isabelle-dev@in.tum.de
https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
Last updated: Dec 21 2024 at 16:20 UTC