Email Gateway (Aug 22 2022 at 12:14): Email Gateway (Aug 22 2022 at 12:14):From: Peter Lammich <lammich@in.tum.de>
First experience with RC1, in the default configuration:
The thing went in a greyout very quickly, on a relatively small project
(approx. 50 files), and the greyout did not recover within reasonable
time.
Essentially, it was only loading $AFP/{Show,Native_Word,Deriving},
before it greyed out.
I'm now trying to copy some settings from Isabelle2015, always
forgetting and having to grab the mail archives to remember what the
crucial settings are, and how they have to be applied.
Email Gateway (Aug 22 2022 at 12:15):From: Peter Lammich <lammich@in.tum.de>
Hi all,
Sorry, this was a false alarm. The thing was stuck at an error on an invalid
theory path quite early in the dependencies. The error was displayed as a
small red bar in the theories panel, but I simply overlooked it ...
Is there another view that is more suitable to spot errors in big projects
with dozens or even hundreds of theories?
Peter
\-------- Originalnachricht --------
Email Gateway (Aug 22 2022 at 12:15):From: Makarius <makarius@sketis.net>
On Thu, 21 Jan 2016, Peter Lammich wrote:
Sorry, this was a false alarm. The thing was stuck at an error on an
invalid theory path quite early in the dependencies. The error was
displayed as a small red bar in the theories panel, but I simply
overlooked it ...
OK.
Also note that the word "grey out" no longer makes sense in Isabelle2016,
because the "greying" is restricted to the small text overview column, so
"out" is not applicable: the main text view remains fully coloured.
Is there another view that is more suitable to spot errors in big
projects with dozens or even hundreds of theories?
The places to look are the Theories panel and the text overview column (of
individual text areas). The latter now shows everything for the document
node, thus it is a small improvement.
Bigger improvements need to wait until there is a separate "Messages"
panel, or similar. It was meant to come shortly after the "State" panel,
but that caused so many social problems that it sucked up much more
resources than anticipated.
In summary: I always need tangible and constructive problem reports; then
things can be improved.
Makarius
Email Gateway (Aug 22 2022 at 12:20):From: Lars Hupel <hupel@in.tum.de>
(This refers to RC2.)
While this is true, the behaviour described by "greyout" still occurs.
In RC2 there is no way I can see when that happens; I just see "stale"
proof state/output/markup and have no idea what's going on.
Cheers
Lars
Email Gateway (Aug 22 2022 at 12:20):From: Makarius <makarius@sketis.net>
Do you have an impression that it occurs less frequently? E.g. due to
various measures in Isabelle2016-RC to require less heap space.
The Monitor panel is now safe to keep open at all time. Maybe you can
keep an eye on the ML heap and tell me later about it.
Makarius
Email Gateway (Aug 22 2022 at 12:21):From: Lars Hupel <hupel@in.tum.de>
Do you have an impression that it occurs less frequently? E.g. due to
various measures in Isabelle2016-RC to require less heap space.
Yes, this is my gut feeling, but not a firm conviction.
The Monitor panel is now safe to keep open at all time. Maybe you can
keep an eye on the ML heap and tell me later about it.
I will try to do that.
Cheers
Lars
Email Gateway (Aug 22 2022 at 12:25):From: Simon Wimmer <wimmersimon@gmail.com>
I second that. Additionally, on RC2 I (Mac OS X) occasionally see a
spinning multi-colored circle, which might stick with me for an indefinite
amount of time during which I cannot make any input. I didn't experience
this with Isabelle 2015.
Email Gateway (Aug 22 2022 at 12:34):From: Manuel Eberl <eberlm@in.tum.de>
I've noticed that, too. Occasionally, especially when loading a large
number of theories inti Isabelle/JEdit (e.g. HOL) and going back and
forth a bit or when letting non-terminating proof methods run for more
than a few seconds, the state output that I get does not get updated
anymore with no indication that it is "stale".
Another recurring problem that I noticed is that sometimes, when loading
e.g. HOL, if one jumps into the middle of one of the theories to be
built while the theories have not all finished building, Isabelle will
start building /all/ of them from the beginning /again/.
This behaviour is somewhat sporadic and despite some effort, I have not
been able to reproduce it properly, so I did not report it before. I
must also admit that I noticed this behaviour with pre-RC Isabelle; I've
not had enough opportunity to use Isabelle enough inbetween to see
whether this occurs with the RC as well, but Lars' and Simon's mail seem
to indicate that it does.
Cheers,
Manuel
Email Gateway (Aug 22 2022 at 12:37):From: Makarius <makarius@sketis.net>
This should normally happen only when the responsibility of 'ML_file'
sources changes from prover to editor. When you click on a source file for
the first time, overall checking recommences at that point.
That is a concession to resource usage. If everything would be managed by
the editor by default, the HOL session could no longer be edited in 8GB
memory.
Makarius
Email Gateway (Aug 22 2022 at 12:44):From: Makarius <makarius@sketis.net>
This is the "beachball of death" by Apple. It means the GUI process is
somehow irresponsive.
There might be a JVM heap problem, when it approaches 100% of the given
limit.
The heap size is shown in the footline in the right corner. If that gets
too high in practical work, you can try with more heap space by editing
Isabelle.app/Contents/Info.plist near the bottom; the default is 2560m.
The application needs to be restarted.
Makarius
Last updated: Apr 16 2024 at 04:18 UTC