Re: [isabelle] RC2 for testing; Toplevel.timing has no affect anymore
On Thu, 10 Oct 2013, Gottfried Barrow wrote:
Any changes to "e spass vampire z3" doesn't stick after I close jEdit. Using
"sledgehammer_params", I see that's the default. I change the default, but
the panel doesn't use them.
The panel picks up global defaults from the prover session, in particular
There are several sources of defaults that might get in conflict, but the
text field has a persistent history (like the one for regular "find" in
jEdit), so you can easily switch back to other items that were used
The panel doesn't give any feedback other than finding a proof, and the
rotating icon, so I'll probably continue to insert a sledgehammer command and
look at the results in the output panel. If no results are coming back, and
the icon is moving, I'm inclined to think it's hung up in a bad way.
I don't understand this part. Do you want to see the command status color
(dark violet) or is there some output of the command that the panel does
SLUGGISH BEHAVIOUR AND BEING UNRESPONSIVE
I think this was mainly because of the Sledgehammer panel running
Sledgehammer when I didn't know it was running.
How many cores do you have?
There can be many things running, either explicitly via panels or
implicitly via automatically tried tools. Sometimes it is difficult to
keep an overview: there could be a central "task manager", but I did not
get that far for this release.
Once I click the Sledgehammer apply button, it will start running again
even after I've hit cancel.
In Isabelle2013-1-RC2 this should work precisely: Apply always makes a
fresh start, Cancel cancels the current sledgehammering, Apply makes again
a fresh start etc.
Sometimes it will start running on its own if I save the file.
This one sounds odd. Did you have it running already? Maybe in a state
where it actually waits for evaluation of the context?
If I hit F11 to maximize the screen, the circular icon will start moving
slowly, but there aren't any ATPs running, so I click "Apply", and then
the circular icon starts moving faster.
I have seen that myself in Isabelle2013-1-RC2, and will investigate it
The current success rate for full-screen mode is a bit more than 50%. On
some platforms it does not work at all, and when it works it can cause
some surprises (like windows that are unreachable somewhere behind the
This archive was generated by a fusion of
Pipermail (Mailman edition) and