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 bottom.

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 Proof General.)

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 next round.

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 MHonArc.