CODEWITHSUNDEEP
isabelle
Joachim Breitner
Joachim Breitner

Reputation: 25763

How to display timing information of proofs in Isabelle

I have a proof by eval that is somewhat slow, and I would like optimize the code. To do so less blindly, it would be great if jEdit could display the time it took to do the by eval proof.

Is that possible with Isabelle 2013?

Upvotes: 1

Views: 194

Answers (1)

user2190811
user2190811

Reputation:

Isabelle can be like Perl, where there's more than one way to do it.

From having seen a few suggestions on the Isabelle user's list, in jEdit, I turn timing information on and off the same way that I turn commands like show_types on and off.

I import a file called i.thy like this:

theory MFZ
imports Complex_Main "../../../../../../ithy/i"
begin

To look at timing information, in i.thy, I have a bunch of information commands, one being the command

ML_command "Toplevel.timing := false"

I set it to true in i.thy, and in my working THY I start changing by statements to apply, and then back to by after I've seen the timing information in the output panel.

To turn the timing information off, you have to change the true back to false. You can't just delete ML_command "Toplevel.timing := true".

If you have a series of apply statements as a proof, you can add the timing sums up, or combine them in one apply/by statement, to get the timing for a single apply statement, like switching the statements

apply(simp)
apply(rule)
by(auto)

to

apply(simp,rule,auto)

To edit commands and change false to true, or vice versa, is probably not much slower than wading through menus to accomplish the same thing.

You could create a jEdit macro to insert the command where you're working, but then you'd have to highlight it and delete it after not needing it any more.

Here's an image of how I keep two views open. The right view shows where I've set Toplevel.timing to true, and the left window shows where I've changed a by to an apply. The image size is 1211x488, and it looks good in Chrome on my end.

http://gc44.github.io/viz/img_1300/130502a__toplevel_timing.png

Upvotes: 2

Related Questions