Re: [isabelle] RC2 for testing; Toplevel.timing has no affect anymore

On 10/11/2013 5:26 AM, Makarius wrote:
How about changing the Threshold for timing display? It is 0.1 seconds by default, so most commands won't show up, since they are much faster.

So I set it to 0, mess around with it a little, and now the timing window becomes an important part of the optimization arsenal.

However, it doesn't help me check the timing for individual "apply" and "by" commands.

The first attached screenshot shows that because the times are ordered from greatest to least, I can't easily associate specific times with specific statements. That's not a good example because it has too few statements in it.

How the timing panel works now is useful, though, because if I want to work on commands that are taking more than 500ms, I can double click on a time in the panel, and it takes me to the statement, which makes for very speedy work.

The second screenshot shows that my work on optimizing time has paid off, which is a result of having used Toplevel.timing to give me timing info.

As shown in the screenshot, with a threshold of 0.0, out of 2292 commands, there's only 12 commands with a time greater than 100ms. In fact, I see a "try" command with 188ms, which I'm using for an example, and I need to comment it out. That's something I would have missed without this new timing panel.

But, with Isabelle2013, when using ML{*Toplevel.timing := true*} or "try", the holy grail of timing was when the time was so short for a statement, the time wouldn't be reported back.

So far, many times, I've started with a proof from an automatic proof method, such as simp, auto, and metis. I then have worked to eliminate those proofs with proof statements that are 30ms or less. Especially now, part of my motivation to use detailed commands, like "rule", is because they're so fast their time doesn't get reported.

If I can figure out a workaround to use the timing panel to compare times for statements of a proof I'm working on, it'll be great. Messing around, I saw that an "apply" and "done" was taking longer than only a "by". I couldn't check that using Toplevel.timing because I had to switch a "by" to an "apply" because it always reported 0 time for a "by".

I'm not asking for any extra features, but statistics would be useful. I got mine above from counting (9 rows x 52 x 4 + 8 rows * 52 + 4). Basic statistics would be great for implicit or explicit bragging rights. Like, it would show I have 40,000 commands in a file, with only 10 commands taking greater than 2ms, resulting in given a title such as "Timing King" or "Timing Guru".


Attachment: timing window ordered.png
Description: PNG image

Attachment: timing with 0 threshold.png
Description: PNG image

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.