Email Gateway (Aug 22 2022 at 09:42): Email Gateway (Aug 22 2022 at 09:42):From: bnord <bnord01@gmail.com>
I observed the following confusing behaviour while porting part of my
development from I14 to I15RC3:
I had some broken mentis calls in some "don't care proofs" so I simply
invoked Sledgehammer there. While Sledgehammer was running the "apply
auto" or "using" right in front of it suddenly was underlined orange and
a couple of "ignoring duplicate rewrite rule" warnings (listing local
facts) popped up in the output. After Sledgehammer finished running the
warning disappeared again.
Another small focus problem which I find confusing: When the
Sledgehammer panel isn't in focus you can mouse over a suggested proof
and it will be highlighted but when you click on it nothing happens
besides switching focus.
Best
Benedikt
Email Gateway (Aug 22 2022 at 09:43):From: bnord <bnord01@gmail.com>
Small follow up,
when selecting a found proof Sledgehammer keeps running and during this
time the syntax highlighting is wrong (apply blue instead of red) and
the inserted command isn't processed until Sledgehammer finished
running/cancelled.
Best
Benedikt
Email Gateway (Aug 22 2022 at 09:43):From: Christian Sternagel <c.sternagel@gmail.com>
Just as a further hint. I experienced the same (only with RC3).
On a (maybe) related note. Whenever I start sledgehammer (through the
panel) and want to do a query (for finding theorems) at the same time,
it seems that I have to wait until sledgehammer is finished before I
obtain any results (this is without moving the cursor after starting
sledgehammer).
Maybe this is just because sledgehammer takes up so many resources that
find_theorems is much slower, or is there a real sequential dependency?
cheers
chris
Email Gateway (Aug 22 2022 at 09:43):From: Makarius <makarius@sketis.net>
This should work in parallel, assuming that free worker threads are
available. Sledgehammer uses as many threads as there are provers.
Find theorems also uses Par_List.map, so it benefits from extra threads,
but does not require them. 1 thread should be sufficient.
Makarius
Email Gateway (Aug 22 2022 at 09:43):From: Makarius <makarius@sketis.net>
This sounds like another episode of the game "funny window managers
against Java/AWT". Just the standard questions:
OS platform?
Window manager?
Java/Swing Look-and-feel?
Makarius
Email Gateway (Aug 22 2022 at 09:43):From: bnord <bnord01@gmail.com>
Am 08.05.15 um 14:38 schrieb Makarius:
OS platform?
OS X 10.10
Window manager?
the "default"
Java/Swing Look-and-feel?
the "default"
Email Gateway (Aug 22 2022 at 09:44):From: Makarius <makarius@sketis.net>
This is an artifact of the internal protocol: Sledgehammer runs as a PIDE
print command, the result is captured by the panel, the print command is
removed. Any uncontrolled warnings that are emitted by the tool in
between are shown in the document view, just like for Auto Sledgehammer,
for example.
The following changesets tighten that aspect of Sledgehammer
https://bitbucket.org/isabelle_project/isabelle-release/commits/d8a4fe35da00
https://bitbucket.org/isabelle_project/isabelle-release/commits/bcd9a70342be
so it should look nicer in the next release candiate.
Makarius
Email Gateway (Aug 22 2022 at 09:44):From: Makarius <makarius@sketis.net>
That is actually a portable cross-platform feature of JDialog.
The easiest way to see the effect is to use the 'help' command and detach
the result as Info window. The main window focused, the detached window
unfocused, a mouse click into the detached window produces a mouse event
on the main window (!), just before transferring focus. Only Oracle knows
what are the reasons for that.
Note that floating doackables used to be based on JFrame in the past, but
that can be much worse: window unreachable behind the main window.
I did not find any further advice on the Web of this focus effect of
JDialog, and the last time I asked about JDialog vs. JFrame vs. JWindow on
stackoverflow, I got removed in a brutal way.
The situation is the same in Isabelle2014, so there won't be any attempts
to refine that detail further in Isabelle2015.
Makarius
Email Gateway (Aug 22 2022 at 09:44):From: Makarius <makarius@sketis.net>
On Fri, 8 May 2015, bnord wrote:
when selecting a found proof Sledgehammer keeps running and during this
time the syntax highlighting is wrong (apply blue instead of red)
I guess that it is right, and the observation merely a change of semantics
in Isabelle2015-RC3 compared to Isabelle2014.
Improper Isar commands like 'apply' are now syntactically like other
commands (blue-ish), and semantically marked-up as "improper" (red-ish).
There is further semantic markup of the same kind for other things, e.g.
rule_tac references to implicit goal parameters.
So I guess that above some 'apply' command in the text became somehow
inactive due to editing, lacking its semantic markup. It should regain
the red hue when it is processed later.
the inserted command isn't processed until Sledgehammer finished
running/cancelled.
I would expect that this works, but there are not enough ML threads ready.
I've just tried it with threads=2 vs. threads=12 on the now infamous
example
lemma "m < n + 1 ⟹ setsum f {m..n + 1} = setsum f {m..n} + f (n + 1 :: int)"
with its rather long-running provers in the background.
Playing with it for a minute, I was satisfied with the scheduling.
Makarius
Email Gateway (Aug 22 2022 at 09:44):From: Lars Noschinski <noschinl@in.tum.de>
These stray warnings had a nice little side-effect for me: They notified
me that sledgehammer had found a proof. As I often switch to the output
or query panels when sledgehammer is busy, this was often useful.
-- Lars
BTW: https://xkcd.com/1172/ ;)
Email Gateway (Aug 22 2022 at 09:45):From: Makarius <makarius@sketis.net>
This well-known cartoon proves that the words "bug" and "feature" are
meaningless.
A problem with the current situation is that we still have too many
"modes" of sledgehammer, some obsolete after the removal of TTY / Proof
General.
Before the change bcd9a70342be, I did not know that the main entry point
of sledgehammer has moved elsewhere. There are more details like
treatment of "using" facts that are unified by it, not just disabling
warnings.
Incremental results can be emitted indepently of that as official
information messages. I don't know why this was not tried before,
probably also because of too much "modes" confusion.
Presently on the release ramp, we should concentrate on the real problems,
such as robust Windows support.
Makarius
Last updated: Nov 21 2024 at 12:39 UTC