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 on startup.

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 before.

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 not show?


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 further.

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 main window).


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