Re: [isabelle] Isabelle2013-2-RC1 available for testing
On Mon, 25 Nov 2013, bnord wrote:
when trying the "lemma False by (intro TrueE)" example on Windows many
times the whole Isabelle interaction seems to freeze, everything from
the previous command becomes a light-gray-pinkish background and there
is no Isabelle output/response whatsoever. Sometimes after running for
several minutes in the background the process seems to recover somehow.
The example of (intro TrueE) is a bit brutal, since it is a
non-terminating execution that allocates more and more ML heap content.
Thus it uses up all CPU and memory resources that the ML process can get:
normally it is only 100% CPU for the ML user task, but the ML runtime
system will use multiple threads for garbage collection and value sharing,
especially when the heap gets tight.
This would explain, why the process is much less reactive to friendly
input messages from Isabelle/Scala to tell the PIDE protocol handler of
Isabelle/ML to terminate certain ML threads, e.g. after some edits.
(It also explains why physical memory eventually fills up on x86_64.)
Waiting several minutes to "recover" might mean two things: (a) you had
some edits to remove the diverging stuff that got eventually accepted, or
(b) the ML task finally evaporated with some internal interrupt exception
due to runtime system overload. In the latter case, we have again the
case that the situation looks good on the surface, but is bad at the
I did not address this second case in the change for Isabelle2013-2-RC1,
since it requires further rethinking how to propagate various kinds of ML
breakdown in the PIDE protocol. There were reasons of not just exposing
all physical failures, due to remaining non-PIDE uses of Isabelle (TTY and
By the way, I could reproduce this under Linux on the same machine (a
little less frequent) and could reproduce it under OS X on a different
machine only when letting the non-terminating command run for a while.
This also left me with a runaway process under OS X which I had to
terminate manually after exiting Isabelle/Jedit.
Just to make sure: the left-over poly process only appeared on Mac OS X,
but not Linux nor Windows?
6 months ago, I discovered by accident that some Ubuntu or Debian
maintainer had changed the command-line of /bin/kill to make it more
modern according to GNU standards, but that "fix" destroyed the
traditional (and presumably portable) kill invocation used Isabelle/Scala.
So I made another (presumably portable) command line for Isabelle2013-1,
which now turns out to be incompatiable with Mac OS X (e.g. Mountain
Lion). This is just the normal POSIX-GNU-BSD non-portability hell ...
I am now addressing this by using the builtin kill command of GNU bash,
which is normally an island of portability in a sea of forks and
divergence. So Mac OS X process termination should be back again in the
Some uncertainty about Windows remains, since Gottfried Barrow had the
impression that termination of external processes was less reliable in
Isabelle2013-1 than Isabelle2013 or Isabelle2012.
This archive was generated by a fusion of
Pipermail (Mailman edition) and