Email Gateway (Aug 23 2022 at 08:51): Email Gateway (Aug 23 2022 at 08:51):From: Peter Lammich <lammich@in.tum.de>
Hi,
I experienced the following odd behaviour for the second time now
(first with RC2, now with RC4), but cannot reliably reproduce it:
When starting Isabelle from the command line, e.g.,
~/opt/Isabelle2020-RC4/bin/isabelle jedit -d ~/devel/isabelle/afp-
devel/thys QBF.thy
jedit will start, and then underline the imported theories with an
error that it cannot load them. Usually, this error goes away after a
few seconds, and Isabelle starts loading the prerequisite theories
(they are, e.g., shown in the Theory panel). This behavior is normal,
also for older Isabelles. However, sometimes, the error will not go
away, and no prerequisite theories will be loaded, even after waiting
for minutes. Also reloading the current file does not help. I have to
quit jedit, and restart.
Anyone observed this behavior? Anything I can do when I encounter it
the next time, to help tracking it down?
Best,
Peter
On Thu, 2020-04-02 at 13:25 +0200, Makarius wrote:
Dear Isabelle users,
the Isabelle2020 release process continues according to plan: the
final and
immutable version will be published on 15-Apr-2020.As a pre-final approximation there is now
available from https://isabelle.in.tum.de/website-Isabelle2020-RC4See again the blog entry
https://isabelle-dev.sketis.net/phame/post/view/5/release_candidates_for_isabelle2020
for further details on cumulative changes.When discussing observations about Isabelle2020 release candidates on
the
mailing list, please provide a "Subject:" line that fits to the
content, not
just a clone of this announcement.Makarius
Email Gateway (Aug 23 2022 at 08:51):From: Lawrence Paulson <lp15@cam.ac.uk>
I think I’ve seen this when there was something badly wrong with the file header initially. And certainly when jedit decides to load an auto-save file: you get the file but can’t do anything with it. I’ve just tested the latter with the development version (df68b82c818d)
Larry
Email Gateway (Aug 23 2022 at 08:51):From: Makarius <makarius@sketis.net>
I was hoping that this rather old behaviour is now gone, but apparently it isn't.
Normally it should be sufficient to edit the theory header, to force an update
of the PIDE document state.
Makarius
Email Gateway (Aug 23 2022 at 08:52):From: Mikhail Chekhov <mikhail.chekhov.w@gmail.com>
Dear All,
I wanted to mention that I observed this behavior for the first at some
point after I started using Isabelle2020-RC2 (I believe, also since I
started using Isabelle2020-RC4). Since then it reoccurred several times,
but I did not find a way to reproduce it reliably. Therefore, I decided not
to post anything about it at the time.
I should mention that I have been using Isabelle consistently for over a
year and, therefore, I used both the stable releases and the release
candidates for Isabelle-2019, as well as the stable release of
Isabelle-2018. I believe that my workflow has not changed since I started
using the software regularly (note that I usually start Isabelle from the
command line). Given that (to the best of my knowledge) it is the first
time that I see this issue, it would be plausible to assume that there was
some regression.
As a side remark, I noticed that the issue seems to never occur if the
first theory that I open after starting Isabelle does not import any
theories that were not built and made available persistently. This is the
practice that I have been following to avoid this issue since I encountered
it several weeks ago. However, upon encountering this issue, the only
solution that I found was to restart Jedit (I believe that I tried closing
and reopening the files and changing/editing the names of the imported
theories).
Kind Regards,
Mikhail Chekhov
Email Gateway (Aug 23 2022 at 08:53):From: Makarius <makarius@sketis.net>
Dear Isabelle users,
the Isabelle2020 release process continues according to plan: the final and
immutable version will be published on 15-Apr-2020.
As a pre-final approximation there is now
available from https://isabelle.in.tum.de/website-Isabelle2020-RC4
See again the blog entry
https://isabelle-dev.sketis.net/phame/post/view/5/release_candidates_for_isabelle2020
for further details on cumulative changes.
When discussing observations about Isabelle2020 release candidates on the
mailing list, please provide a "Subject:" line that fits to the content, not
just a clone of this announcement.
Makarius
Last updated: Apr 16 2024 at 20:15 UTC