Email Gateway (Aug 19 2022 at 12:44): Email Gateway (Aug 19 2022 at 12:44):From: Makarius <makarius@sketis.net>
Dear Isabelle users,
this is yet another release candidate for the second attempt to make a
stable release of Isabelle this autumn:
http://isabelle.in.tum.de/website-Isabelle2013-2-RC2
The final Isabelle2013-2 should appear next week, unless further problems
show up.
Notable changes versus Isabelle2013-2-RC1:
* Reactivated Isabelle/Scala kill command for external processes on Mac
OS X (e.g. poly), after 6 months of suffering from some Ubuntu/Debian
Linux workaround that did not take Apple's BSD into account.
* More status information about commands that are interrupted
accidentally (via physical event or Poly/ML runtime system signal,
e.g. out-of-memory).
* Second attempt to get ML task termination right, while the user
continues editing.
There should not be any incompatibilites wrt. Isabelle2013-1, which means
everybody who is already on the latest release can try out the new release
candidate without any extra efforts.
Ongoing changes were motivated by a really stable release of
Isabelle/jEdit, but such delicate details of Isabelle command execution
can also affect TTY and Proof General. I've have made some basic tests of
the latter, but have problems recalling how manual script management used
to work.
Observations from testing release candidates may be discussed here on
isabelle-users (not isabelle-dev), on the bitbucket tracker
https://bitbucket.org/isabelle_project/isabelle-release/issues or via
private mail.
Makarius
Email Gateway (Aug 19 2022 at 12:44):From: bnord <bnord01@gmail.com>
Hi,
process termination upon exit now seems to work well under OS X.
I still could get the Isabelle interaction to 'freeze' after
continuously editing after a non-terminating "by (intro TrueE)" for
about 30 seconds. So the situation is greatly improved compared to RC1.
I then waited for about 5 minutes without any change, then after
removing the non-terminating command it required waiting about 2 minutes
until the command was finally interrupted and interaction came back.
Best
Benedikt
P.s. This isn't a regression but when hovering over items in the
Sidekick panel the height of the status bar changes and causes half of
the UI to 'jump' around.
Email Gateway (Aug 19 2022 at 12:45):From: Makarius <makarius@sketis.net>
As long as it comes back eventually, it is not fully frozen. And
hopefully, there is not another serious problem waiting at the bottom of
it.
I've experimented myself a bit with (intro TrueE): after several seconds,
when the process exceeds 1-2 GB heap size, it takes really long to react
on interrupts. This is probably due to garbage collection and value
sharing of Poly/ML, trying to catch up with this non-terminating
allocation process.
Makarius
Email Gateway (Aug 19 2022 at 12:47):From: "Yannick Duchêne (Hibou57 )" <yannick_duchene@yahoo.fr>
Don't know if it's the place to tell: there is a typo in “tutorial.pdf”.
In “8.3.1 Overloading”, it says:
We can introduce a binary infix addition operator ⊗
While it should be
We can introduce a binary infix addition operator ⊕
Also, while I'm not to beg it, just as a suggestion only if it's possible:
when the “Symbols” pan is docked at the bottom of the Isabelle text pan,
it could be handy if the text pan could scroll so that the position at the
caret is always visible. Actually, if the caret is near the bottom of the
text pan, then pushing the “Symbols” button to show the symbols pan, the
latter may hide the text where the caret is located, which is not very
pleasant.
Email Gateway (Aug 19 2022 at 12:47):From: "Yannick Duchêne (Hibou57 )" <yannick_duchene@yahoo.fr>
Another UI related tiny one: when on the “Documentation” pan, I click on
document a row, then close the PDF reader, then click again on the same
row, the document does not opens any‑more. I have to click on another row,
then click on the former again. I guess that's because jEdit can't know if
the document is still opened, and probably it supposes it still is, and in
such a case, a click on the row which is already selected, is probably
supposed to result into the document opened twice. So, may be an option
could be to be able to reopen a document whose row is already selected,
with a double‑click, instead of a single‑click (and to keep the
single‑click to open a document whose row is not selected).
Note: I'm running Ubuntu 12.04 LTS 32 bits, if ever that matters and as I
don't know if the behaviour I described above occurs on all platforms.
Email Gateway (Aug 19 2022 at 12:55):From: bnord <bnord01@gmail.com>
It shouldn't suppose such things, if I click on the documentation I want
it to open. Think the problem is that the document is opened when the
item is selected not when it's clicked on, if you use the arrow keys to
select a documentation, all documentations on the way are opened ;)
Related problem: on OS X for each documentation a new instance of my
viewer is started instead of reusing the old instance as customary under
OS X, why don't you just use OS X's "open" command which handles all this?
Best Benedikt
Email Gateway (Aug 19 2022 at 12:56):From: "Yannick Duchêne (Hibou57 )" <yannick_duchene@yahoo.fr>
Don't know if it's just me, here is anyway: in the outline in the
Sidekick, the keyword “end” appears for each construct terminated with an
“end”. It's a bit like noise. May be an option could be to filter out this
“end” or else tell the parser to handle “end” as if it was inside the
construct.
Email Gateway (Aug 19 2022 at 13:02):From: bnord <bnord01@gmail.com>
Thanks,
after changing this to plain "open" it works as I'd expect it. The "-n"
option was the one causing the /trouble/, without this the "-W" made
little sense I guess (does anything depend on this behaviour?). I also
removed the "-F" so I don't accidentally lose my old session when
opening my first PDF via Isabelle. Why is it there anyway? I don't think
open would restore the session of there is already some instance running.
Two additional minor remarks:
It would be nice if Isabelle would ask one whether it should "copy"
the existing configuration from some old version upon first start.
On the download page there is additional underlined white space at
the end of the "Download for Linux " link when viewed from OS X. ;)
Best Benedikt
Email Gateway (Aug 19 2022 at 13:05):From: Makarius <makarius@sketis.net>
I have experimented with this once again on all platforms, using present
day desktop integration tools uniformly: xdg-open, cygstart, open ---
always in asynchronous mode without forcing it elsewise.
This seems to work better by default than our old synchronous scheme,
which was motivated by situations that hardly exist anymore. The remaining
use of this old-fashioned PDF_VIEWER invocation is the 'display_drafts'
command, but that only makes sense in legacy TTY mode.
Isabelle/jEdit is much better at displaying the "draft" of source files
with Isabelle symbols directly on the screen, and its buffer print
function does a surprisingly good job with the IsabelleText font.
So we have again reduced the problem to Proof General / Emacs :-)
Makarius
Email Gateway (Aug 19 2022 at 13:06):From: Makarius <makarius@sketis.net>
On Sun, 1 Dec 2013, bnord wrote:
Am 01.12.2013 00:07, schrieb Yannick Duchêne (Hibou57):
I guess that's because jEdit can't know if the document is still opened,
and probably it supposes it still is, and in such a case, a click on the
row which is already selected, is probably supposed to result into the
document opened twice.
It shouldn't suppose such things, if I click on the documentation I want it
to open. Think the problem is that the document is opened when the item is
selected not when it's clicked on, if you use the arrow keys to select a
documentation, all documentations on the way are opened ;)
There are a variety of accidental and fundamental Java GUI vs. OS desktop
environment problems here that I did not manage to sort out in every
respect for the Isabelle2013-1 / Isabelle2013-2 release. It is already an
improvement that documentation is readily available at all, which was not
the case in the years before.
What I usually do myself is to click on one of the "section" entries as a
resting position, and then make a fresh click on the piece of
documentation that should open once again. (Silly if one needs extra
documentation to browse documentation efficiently.)
Related problem: on OS X for each documentation a new instance of my
viewer is started instead of reusing the old instance as customary under
OS X, why don't you just use OS X's "open" command which handles all
this?
I have struggled a long time with that odd detail. Since we only support
Lion or later, the settings for it are now as follows:
PDF_VIEWER="open -W -n -F"
This agglomeration of options stems from several years working around
defaults by Apple, but the final -F is brand new.
You can change the above in $ISABELLE_HOME_USER/etc/settings and see if
other forms work better. (Changing system settings needs a restart of the
application each time.)
Makarius
Email Gateway (Aug 19 2022 at 13:09):From: Makarius <makarius@sketis.net>
I have changed that on
https://bitbucket.org/isabelle_project/isabelle-release/ for the final
Isabelle2013-2 release. (Afterwards the change will come back on the main
Isabelle repository by the canonical merge.)
Note that the "tutorial" is generally not quite up-to-date --- smaller or
bigger mistakes and confusion can happen.
Makarius
Email Gateway (Aug 19 2022 at 13:09):From: Makarius <makarius@sketis.net>
Whatever happens here is standard jEdit behaviour of the so-called
"Dockable Window Manager". It is used a lot in Isabelle/jEdit, and it
does a good job up to a certain point.
I have my own list of possible improvements here, but it needs to be
sorted out at http://sourceforge.net/projects/jedit/
Makarius
Email Gateway (Aug 19 2022 at 13:09):From: Makarius <makarius@sketis.net>
Current Isabelle SideKick does not take any structure of Isar commands
into account, neither proof blocks nor begin/end within theory
specifications. Only some document markup commands are handled: chapter,
section, subsection etc., which sometimes helps a little to keep an
overview.
Right now the SideKick mode for the Isabelle NEWS file is of more
practical importance.
Makarius
Email Gateway (Aug 19 2022 at 13:16):From: "Yannick Duchêne (Hibou57 )" <yannick_duchene@yahoo.fr>
Yes! I was to thank for that too, but I forget. That's handy for seasoned
users, so thanks.
Last updated: Nov 21 2024 at 12:39 UTC