Email Gateway (Aug 19 2022 at 12:02): Email Gateway (Aug 19 2022 at 12:02):From: Makarius <makarius@sketis.net>
On Thu, 10 Oct 2013, Gottfried Barrow wrote:
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 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?
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
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).
Makarius
Email Gateway (Aug 19 2022 at 12:04):From: Makarius <makarius@sketis.net>
I now understand better what F11 (toggle full-screen mode) does here.
The deeper problem is that the state of the Sledgehammer panel is managed
in accordance to its GUI representation, but that is reset a bit more
often than anticipated. When you toggle full-screen mode, the panel is
removed and added again, so the Sledgehammer run is reset. In
Isabelle2013-1-RC2 the GUI display is a bit crude and merely changes into
the state "Waiting for evaluation of context ...". In the coming RC3 this
week it will be more clear that the state is reset.
These slight inconveniences of dockable window state are due to certain
features of Java/Swing and jEdit Dockable Window Management. For Output
and Info, I had already made some workarounds a few years ago, to pretend
more persistence than is there in reality. Instead of adding more
workarounds it would be better to brush up the Dockable Window Manager at
some point, but it requires some enthisiastic and competent people helping
out at the jEdit project on Sourceforge.
Another known problem of dockable windows (especially in full-screen mode)
is that windows often get lost behind the main window. The precise
behaviour is platform dependent.
Makarius
Email Gateway (Aug 19 2022 at 12:05):From: Makarius <makarius@sketis.net>
The old Toplevel.timing produced a plain-text message that was printed for
the corresponding command. You can get similar output as tooltip now.
Here is a clarified NEWS entry for the release:
Does that address all problems and confusions?
Makarius
Email Gateway (Aug 19 2022 at 12:05):From: Makarius <makarius@sketis.net>
"RC" means "release candidate", not "release". We are presently at
release candidate #2, working towards just one final release called
"Isabelle2013-1" (according to the canonical Isabelle release naming
scheme).
And yes, the NEWS item refers to what you see in Isabelle2013-1-RC2
already. I merely updated the NEWS to make more clear how it works.
I've also tried once again on Windows that timing of some 'apply' command
also works. Of course, you need to set the timing threshold to something
that is sufficiently small (even 0.0).
Makarius
Email Gateway (Aug 19 2022 at 12:05):From: Makarius <makarius@sketis.net>
On Mon, 14 Oct 2013, Gottfried Barrow wrote:
It would be nice to have the "using[[blast_trace]]" back.
I've rarely used blast, or so I thought, but now that I see that auto
calls it a lot, I see I've been using it a lot all along.You say the blast trace is not meant for user consumption, but I'm using
it.
That was just an accident. You found some funny flag and used it for some
odd purpose, without any general principle behind it. For every Isabelle
feature there need to be 2 or 3 good reasons to be there.
The following user-space attribute definition defines something that is
close to the discontinued blast_trace declaration:
attribute_setup blast_trace = {*
Scan.succeed (Thm.declaration_attribute (K (Config.put_generic Blast.trace true)))
*}
lemma "A ⟶ A" using [[blast_trace]] by blast
Here is also a slightly more elaborate version with argument parser:
attribute_setup blast_trace = {*
Scan.lift
(Parse.$$$ "=" -- Args.$$$ "true" >> K true ||
Parse.$$$ "=" -- Args.$$$ "false" >> K false ||
Scan.succeed true) >>
(fn b => Thm.declaration_attribute (K (Config.put_generic Blast.trace b)))
*}
These Isabelle/ML operations are much less arcane than the use of
blast_trace in the first place.
It's also not about proving the theorem. It's about learning something
from the blast method. I allocate a few minutes to look at the HOL.impCE
that it lists in the details.
Blast is a slightly more sophisticated version from the basic Classical
Reasoner. The latter is definitely worth learning, using its fine
documentation in the isar-ref manual and its ML sources.
Makarius
Email Gateway (Aug 19 2022 at 12:06):From: Makarius <makarius@sketis.net>
There is a more serious socket problem behind this, see also
https://bitbucket.org/isabelle_project/isabelle-release/issue/19/unreliable-socket-communication-leads-to
I've spend 1-2 days looking through the socket implementation of Poly/ML
and Java/Scala and TCP/IP manual pages. It is still unclear what can be
done. The problem only manifests itself in relatively rare situations,
i.e. an empty edit following the options change, which explains why it was
not noticed before.
Another reason why it was overlooked is that people on isabelle-dev rarely
use Windows. But Linux and Mac OS X also have their own problems in
different departments. I reckon that the amount of issues and annoyances
is approximately equal on all 3 platforms now.
I hope to make Isabelle2013-1-RC3 tomorrow, probably without any change in
that corner. Then I am on vacation from 17-Oct..04-Nov. Afterwards comes
the final round for final lift-off of the Isabelle2013-1 release.
Makarius
Email Gateway (Aug 19 2022 at 12:25):From: Makarius <makarius@sketis.net>
How about changing the Threshold for timing display? It is 0.1 seconds by
default, so most commands won't show up, since they are much faster.
Makarius
Email Gateway (Aug 19 2022 at 12:25):From: Makarius <makarius@sketis.net>
That low-level approach to inspect document markup is obsolete, as far as
timing is concerning.
Slowness or unresponsiveness here might mean you just have a very big text
with lots of markup. If there are other reasons for that, there might be
a genuine problem, but from the description so far there is no indication.
Makarius
Last updated: Apr 23 2024 at 16:19 UTC