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



I'm using Cygwin.

NO TIMING INFO ANYMORE

The "Timing" panel doesn't seem to work. Some timing comes up for a few commands, but they're not related to where I'm at in the document, and they don't change for the most part.

The command "ML{*Toplevel.timing := false*}" has no affect anymore. I love timing proofs.

SIDEKICK AND ISABELLE-MARKUP

I try to get timing from using "isabelle-markup" in the drop-down box in Sidekick, but it's very unresponsive, and it's hard to get the tree expanded in sync with where I'm at in the document, so it doesn't work.

SLEDGEHAMMER PANEL

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

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.

Once I click the Sledgehammer apply button, it will start running again even after I've hit cancel. Sometimes it will start running on its own if I save the file.

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.

PINK SCREEN AFTER OPTIONS CHANGES

When I change any "Plugin Options" and then hit apply, the text will be purple until I scroll the screen a little. When I'm having problems, and turning the auto checkers on and off to see if they're causing the problem, I can think the purple text after the option change is related to the problems I'm having.

Regards,
GB














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