Email Gateway (Aug 19 2022 at 12:48): Email Gateway (Aug 19 2022 at 12:48):From: Makarius <makarius@sketis.net>
Dear Isabelle users,
here is another release candidate:
http://isabelle.in.tum.de/website-Isabelle2013-1-RC4
This is probably the last one before final lift-off next week.
Notable changes wrt. Isabelle2013-1-RC3:
* Minimal tuning of Isabelle/HOL library and tools.
* Minimal tuning of some Isabelle/jEdit GUI aspects.
* More documentation for Isabelle/jEdit (25 pages manual).
* Proper join of forked diagnostic commands in Proof General theory
loader.
* Update to Poly/ML 5.5.1 with commits 1869 (fix two optimiser bugs) and
1875 (allow IO request of zero characters).
See also https://bitbucket.org/isabelle_project/isabelle-release for the main
website where the final stage before Isabelle2013-1 is organized. There is also
a link to an issue tracker on the same Bitbucket site.
Observations from testing release candidates may be discussed here on
isabelle-users (not isabelle-dev), on the bitbucket tracker, or via private
mail.
It only makes sense to test the latest release candidate. People who
have provided some form of feedback should update and check how that
aspect is now treated -- sometimes a last-minute attempt to improve things
actually goes into the opposite direction.
Major operating system vendors have now released their latest versions as
well: Ubuntu 13.10, Windows 8.1, Mac OS X 10.9. So this is an opportunity
to see that everything fits nicely together.
Makarius
Email Gateway (Aug 19 2022 at 12:49):From: Makarius <makarius@sketis.net>
I would like to raise attention to the following timing problem with
keyboard events vs. completion popup focus:
https://bitbucket.org/isabelle_project/isabelle-release/issue/22/underscore-swallowed-when-autocompletion
Is Joachim Breitner just very fast in typing, or did other people
experience the same?
Makarius
Email Gateway (Aug 19 2022 at 12:50):From: Gottfried Barrow <gottfried.barrow@gmx.com>
Hi,
After I've run Sledgehammer once in the panel by clicking "Apply", it
will run on its own, and here is the description:
The following is in the file Scratch.thy, in a new Cygwin installation
in which I've changed no options.
theory Scratch
imports Complex_Main
begin
theorem "A = A"
oops
end
I place my cursor after "A = A", I click "Apply", Sledgehammer runs, and
it returns "Try this: by metis (1 ms)" for e, spass, remote_vampire, and
that I need to change "Z3_NON_COMMERCIAL" to yes.
I place my cursor at the empty line before "theorem", hit the space bar,
Sledgehammer runs again on its own, returns the same results, and it
terminates like it should.
So, I can edit anything after "A = A", but if I make any edits before
"theorem", it runs on its own, even if I click on a proof so that it's
inserted. This happens every time after I exit and restart jEdit, and
there are no other files open.
There's also no persistence in the "Provers" field. The "Previously
entered strings" is always empty, no matter how many times I've edited
the field. I don't care about that. I'm just reporting it.
Regards,
GB
Email Gateway (Aug 19 2022 at 12:50):From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
Dear Makarius,
I also experienced that popups swallow characters, and it happens with all characters, not
just underscores. For me, it most likely happens when Isabelle works a lot in the
background. My system parameters: standard 12.04 LTS Ubuntu Linux.
Andreas
Email Gateway (Aug 19 2022 at 12:51):From: Makarius <makarius@sketis.net>
I've made some re-adjustements after the Isabelle2013-1-RC4 snapshot: see
https://bitbucket.org/isabelle_project/isabelle-release version
9c1f21365326. Can you give it a quick try? You know how to work with
repository versions.
The documentation for the change is like this:
\item The system option @{system_option
jedit_completion_dismiss_delay} determines an additional delay (0.0
by default), before dismissing an earlier completion popup. A value
like 0.1 is occasionally useful to reduce the chance of loosing key
strokes when the speed of typing exceeds that of repainting GUI
components.
My impression is that Linux users who type very quickly are apt to see the
problem with some probability. On Windows, the Java GUI performance is
much better, but I've seen the same when running a remote Windows session
over a slow connection.
The next time I pass by the completion mechanisms, I will remove any
attempts to do a GUI focus change. After studying the AWT/Swing
documentation and sources quite some time, I came to the conclusion that
this is inherently difficult to get right, despite some explicit
mechanisms to queue/dequeue "typeahead key events" in the AWT event
handler.
What I actually wanted to do last summer was to provide context-sensitive
completion, based on information provided by the prover. Then I got stuck
with many such GUI issues, and these timing problems are just the last
bits of it.
Makarius
Email Gateway (Aug 19 2022 at 12:51):From: bnord <bnord01@gmail.com>
Hi,
I could reproduce this also on OS X 10.9 but had to try really hard.
Same on Ubuntu 12.04
One observation:
I also reproduced this programmatically and observed that keys only get
lost not when the popup opens but after the point where the next
possible character is the same for the remaining possible keywords that
is the "_" in find_theorems or the "t" in print_theorems. Maybe the
problem is not with the popup itself?
Best Benedikt
Email Gateway (Aug 19 2022 at 12:51):From: Makarius <makarius@sketis.net>
This is consistent with my understanding of AWT/Swing focus transfer,
after studying the documentation and sources for 1-2 days. The problem is
that "type-ahead" buffering only works for one new GUI component at a
time. The Isabelle/jEdit can open and close many of them in a row rather
quickly. Thus queue events may get redirected to already closed popups.
This is why I've added jedit_completion_dismiss_delay right after
Isabelle2013-1-RC4.
I am merely waiting for at least one guy who types very fast to confirm
that jedit_completion_dismiss_delay=0.1 prevents the problem most of the
time. (Otherwise I have to make yet another release candidate, and
postpone the final lift-off by a few more days.)
Makarius
Email Gateway (Aug 19 2022 at 12:51):From: Makarius <makarius@sketis.net>
On Sun, 10 Nov 2013, Gottfried Barrow wrote:
After I've run Sledgehammer once in the panel by clicking "Apply", it will
run on its own, and here is the description:I place my cursor after "A = A", I click "Apply", Sledgehammer runs, and it
returns "Try this: by metis (1 ms)" for e, spass, remote_vampire, and that I
need to change "Z3_NON_COMMERCIAL" to yes.I place my cursor at the empty line before "theorem", hit the space bar,
Sledgehammer runs again on its own, returns the same results, and it
terminates like it should.
That is an interesting corollary of sledgehammer as "query operation".
The sledgehammer invocation is associated with a "document overlay", based
on the static command 'theorem', and it remains there until you invoke it
differently. So when you edit before that command, it is re-checked
together with its sledgehammer overlay.
This gives the effect of "run on its own". The "Cancel" button is not
sufficient to remove the potential sledgehammer run, it only refers to the
current dynamic execution of it. So to dispose sledgehammer permanently,
you need to apply it elsewhere (e.g. outside a proof context), or undock
the panel.
There's also no persistence in the "Provers" field.
The persistence is in the history of the text field. This is also useful
to "park" several sets of options that are commonly used.
Makarius
Email Gateway (Aug 19 2022 at 12:51):From: Joachim Breitner <breitner@kit.edu>
Hi,
sorry, I wasn’t aware that there was not another RC upcoming. Fetched
and built 9c1f21365326, and indeed, with
jedit_completion_dismiss_delay=0.1 I could not reproduce it, neither
manually nor with xdotool. It looks a bit weird to see multiple popups,
but definitely better than disappearing key presses.
Thanks for finding a work-around,
Joachim
signature.asc
Email Gateway (Aug 19 2022 at 12:52):From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
Hi Makarius,
It seems to be gone with value 0.1.
Andreas
Last updated: Apr 24 2024 at 20:16 UTC