Stream: Mirror: Isabelle Users Mailing List

Topic: [isabelle] Profiling time?

view this post on Zulip Email Gateway (May 22 2021 at 09:19):

From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
Hi all,

I aim to get some time samples for locale activation and my first
entrance point is ML_Profiling.profile_time, with a naive modification
of locale.ML:

fun print (k, s) = string_of_int k ^ " " ^ s;
fun prints kss = (map print kss; ());

fun activate_all name thy activ_elem transfer (marked, input) =
ML_Profiling.profile_time_thread prints (activate_all' name thy activ_elem transfer) (marked, input)

Anyway, the build of the HOL image fails erratically with sth like

*** exception Fail raised (line 506 of "profiling.cpp"): Profiling is currently active
*** At command "class" (line 93 of "~~/src/HOL/Complete_Lattices.thy")

presumably due to parallelism.

Am I on the right path for timing samples or should I try sth else, e.
g. from timing.ML?

Cheers,
Florian
OpenPGP_signature

view this post on Zulip Email Gateway (May 22 2021 at 10:28):

From: Makarius <makarius@sketis.net>
The 3 combinators in ML_Profiling are provided by the Poly/ML run-time system
and allow detailed and low-level profiling.

I often use 2 of them indirectly via "isabelle build -o profiling=time" or
"... -o profiling=allocations". The allocations are actually more useful,
since most of our run-time is spent in producing new functional data
structures. Reading the tea leaves within that trace can reveal where
performance problems really are.

ML_Profiling.profile_time_thread is special, because it is restricted to a
single thread and measures its CPU time accurately. It should work properly
together with "... -o threads=1".

Makarius

view this post on Zulip Email Gateway (May 27 2021 at 12:51):

From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
I am still somehow lost on how to actually apply profiling

I have defined a dedicated session »profile« that I want to profile.

But after a

isabelle build -o profiling=allocations profile

neither

isabelle profiling_report

nor the slightly more explicit

isabelle profiling_report heaps/polyml-5.8.2_x86_64_32-linux/log/profile.gz

emit anything.

What am I missing?

Thanks a lot,
Florian
OpenPGP_signature

view this post on Zulip Email Gateway (Jun 12 2021 at 10:24):

From: Makarius <makarius@sketis.net>
This actually does not quite work in Isabelle2021, due to the change of the
build process to use a PIDE session: messages end up elsewhere.

For the next release, I have reworked the overall setup, see
https://isabelle-dev.sketis.net/phame/post/view/39/reactivated_ml_profiling

Makarius

Last updated: Jan 04 2025 at 20:18 UTC