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
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
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
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.
This archive was generated by a fusion of
Pipermail (Mailman edition) and