Stream: Mirror: Isabelle Development Mailing List

Topic: [isabelle-dev] NEWS: Reactivated ML profiling


view this post on Zulip Email Gateway (Jun 09 2021 at 12:01):

From: Makarius <makarius@sketis.net>
* System *

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: Mar 29 2024 at 08:18 UTC