Re: [isabelle] Isabelle2013-RC2 available for testing



So Sledgehammer is back in the saddle again. I run 13 ATPs together, and the ATPs that normally find proofs all return normally. If I run 24 ATPs together, then it seems to cause some of the ATPs to time out or terminate when they otherwise wouldn't, but they terminate in a normal manner by returning an error message.

Getting analytical about the output panel, I'd say there are two types of information, primary information and secondary information.

With Sledgehammer set for a 60 second timeout, the output is always going to be primary information, meaning that I'm always going to want to look at the output from the time I start the command until the command finishes.

It turns out that I've switched today to using the tooltip window to look at the Sledgehammer window, since it doesn't get overwritten with new data while Sledgehammer is running.

The cycle is something like this:

1) Start Sledgehammer.

2) Hover over "sledgehammer".

3) When the tooltip window pops up, click on the "Detach tooltip window" icon so that it's a normal window and doesn't disappear if I click somewhere else.

4) Scroll to the bottom to see if there's any new output there to think about, and maybe go ahead and click on a proof to insert it and terminate Sledgehammer.

5) Close the window.

6) Loop through items 2 through 5 until sledgehammer finishes, and then do it one last time.

So, I use whatever features are there to be used. If the output panel went away, I obviously wouldn't use it.

But some information you want to look at a lot, and some information you only want to look at on an as need basis. So if you have to do more work than you used to to look at information that you look at a lot, then you will long for yesterday.

Regards,
GB









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