Re: [isabelle] RC1 - Greyout
- To: cl-isabelle-users at lists.cam.ac.uk
- Subject: Re: [isabelle] RC1 - Greyout
- From: Manuel Eberl <eberlm at in.tum.de>
- Date: Tue, 2 Feb 2016 08:59:58 +0100
- In-reply-to: <CAASQnwP-LVYv2u27DTTw5xO8k8UsLDoem5oMx7jw=RGohNm2Hw@mail.gmail.com>
- References: <Z005fbs0LF6xvh2.RZmta@smtpin.rzone.de> <alpine.LNX.firstname.lastname@example.org> <56A896B2.email@example.com> <CAASQnwP-LVYv2u27DTTw5xO8k8UsLDoem5oMx7jw=RGohNm2Hw@mail.gmail.com>
- User-agent: Mozilla/5.0 (X11; Linux x86_64; rv:38.0) Gecko/20100101 Thunderbird/38.5.1
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.
On 27/01/16 11:17, Simon Wimmer wrote:
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.
This archive was generated by a fusion of
Pipermail (Mailman edition) and