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



FROM THERE: Re: [isabelle] No blast_trace anymore; assumption trace?
setup "Config.put_global Blast.trace true"

That is a rather indirect way to see when blast happens to be invoked by other proof tools. Generally, producing a meaningful trace is very difficult for anything non-trivial.

Thanks for the command. If you tell me other ways to know when one method is calling another, I'll make a note of it, but even though there's some information overload with the blast trace, it showed me that auto may be doing more than what the simp trace shows. Given enough time, I'll use the blast trace to get more awareness about this "classical reasoner" business.

BACK TO HERE:
On 10/11/2013 6:00 AM, Makarius wrote:
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.

I'm not getting any persistent history. When I was first trying out the new features, "Find" did record some search words I typed in, but now "Find" is not even remembering any new search strings.

I copy the unpacked "Isabelle2013-1-RC2.exe" to another location and start it with batch files to set home folders, so I've also been testing the default install, with very few option changes. The default install uses "e spass remote_vampire z3", where my customized install doesn't use remote_vampire, but it uses ""e spass vampire z3"".

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?

This is related to the fact that I use the option "verbose=true" with my normal Sledgehammer commands, which I wasn't considering.

Sledgehammer normally doesn't behave bad anymore as far as not terminating, but it's taken over the CPU enough times in the past, that's the first thing I start thinking about if it gives the appearance it's not working right.

With "verbose=true", it puts out a lot of information, which helps me see that it's probably working right. When all the panel does is display proofs that it finds, and it doesn't return any info in 30 seconds or more, I start wanting to terminate it.

It's not just that, though. The verbose information is a big part of how I make decisions on whether to let Sledgehammer keep running. I don't run Sledgehammer in the background while I'm working on something else. If it takes it 3 minutes to find a proof, then it's probably a 3 minute long proof, which has so far been worthless to me. If I don't get reasonably fast results from Sledgehammer, like within a minute, my theorem is probably false, or I haven't set things up right with my lemmas.

I also look get lots of information I look at before it totally finishes. I'm constantly detaching the output panel to look at what it has produced, while it's still running. With Sledgehammer, so far, I'm always focused on using it to try a finish the current proof I'm working on, and the verbose info is part of that.

So no verbose feedback from the panel doesn't let me work the way I like to work.

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?

This ties into the last paragraphs above. Sledgehammer is not a lightweight prover, other than maybe the 2-second auto tool setting, which I'm not using. The default timeout for the panel is 30 seconds, and I have my command set to 60 seconds with 11 ATPs to run. With a long timeout, all four cores frequently run at 100%.

I have an older 2.8GHz 4-core, non-i7. In the case of newly experimenting with RC2, I was trying to make comparisons between the panel Sledgehammer and my normal Sledgehammer commands. I think the Sledgehammer panel was starting up on its own after I had hit "Cancel", and I was starting my usual heavy duty Sledgehammer commands, so the CPU was getting way overloaded.

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.

I have 4 CPU meter icons in my task bar, but I can fail to notice that they're all maxed out when I'm trying to figure out why I'm having problems.

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?

I couldn't duplicate the panel starting on its own when saving a file, except the period of time when I was starting lots of Sledgehammer commands from the panel and in the buffer. I had to terminate a bunch of processes, and I haven't had a big problem like that again. I thought maybe the F11 screen maximize problem might be related, so I described that.

Regards,
GB






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