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