Stream: General

Topic: Profiling, i.e. finding the proof steps, that take long

Moritz R (Mar 24 2025 at 20:50):

Is there any way to show the proof steps that take the longest?
I have a theory, that takes too long to check for my preference, and i would like to optimize the biggest slouches first.
The "method" i have been using is
"compile the whole file, and see where the checking stays for the longest".

I noticed, that sometimes (but only sometimes? is it only for steps taking longer than 300ms or so?) one can hover over by and get a reading how many (milli)seconds the proof needed.

Is there any better way to do this?

Mathias Fleury (Mar 24 2025 at 20:53):

timing panel

Mathias Fleury (Mar 24 2025 at 20:53):

Plugins > isabelle > timing panel

Moritz R (Mar 24 2025 at 20:59):

ohh there is more panels!

Moritz R (Mar 24 2025 at 21:00):

But how does one use this panel? It only enumerates that some by command took x seconds, but it doesnt tell me which one

Mathias Fleury (Mar 24 2025 at 21:01):

you can double click on the bars

Mathias Fleury (Mar 24 2025 at 21:01):

to find which command it corresponds to

Moritz R (Mar 24 2025 at 21:02):

perfect!

Moritz R (Mar 24 2025 at 21:02):

This is exactly what i was searching for, thank you!

Last updated: Apr 26 2025 at 12:36 UTC