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?
timing panel
Plugins > isabelle > timing panel
ohh there is more panels!
But how does one use this panel? It only enumerates that some by command took x seconds, but it doesnt tell me which one
you can double click on the bars
to find which command it corresponds to
perfect!
This is exactly what i was searching for, thank you!
Last updated: Apr 03 2025 at 20:22 UTC