Email Gateway (Aug 19 2022 at 12:39): Email Gateway (Aug 19 2022 at 12:39):From: Makarius <makarius@sketis.net>
Dear Isabelle users,
this is another attempt to make a stable release of Isabelle this autumn:
http://isabelle.in.tum.de/website-Isabelle2013-2-RC1
This is presumably the only release candidate before final lift-off of
Isabelle2013-2 in the first days of December.
Notable changes versus Isabelle2013-1 (from NEWS):
* Prover IDE -- Isabelle/Scala/jEdit *
More robust editing of running commands with internal forks,
e.g. non-terminating 'by' steps.
More relaxed Sledgehammer panel: avoid repeated application of query
after edits surrounding the command location.
There should not be any incompatibilites wrt. Isabelle2013-1, which means
everybody who is already on the latest release can try out the new release
candidate without any extra efforts.
See also https://bitbucket.org/isabelle_project/isabelle-release for the
main website where the Isabelle release process is formally organized.
There is also a link to an issue tracker on this Bitbucket site.
Observations from testing release candidates may be discussed here on
isabelle-users (not isabelle-dev), on the bitbucket tracker, or via
private mail.
Makarius
Email Gateway (Aug 19 2022 at 12:39):From: bnord <bnord01@gmail.com>
Hi,
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.
Best
Benedikt
Email Gateway (Aug 19 2022 at 12:39):From: bnord <bnord01@gmail.com>
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.
Best
Benedikt
Email Gateway (Aug 19 2022 at 12:39):From: Makarius <makarius@sketis.net>
Which runaway process, poly or java?
Can you also give a rough hardware specification of the test machines?
Makarius
Email Gateway (Aug 19 2022 at 12:39):From: Peter Lammich <lammich@in.tum.de>
I have the same effect under Linux(Ubuntu) occasionally,
but no reliable way how to reproduce.
Email Gateway (Aug 19 2022 at 12:40):From: bnord <bnord01@gmail.com>
The runaway process is poly.
The win/linux test machine is a Intel Core i5-3570 with 8GB of ram
running Windows 8.1 resp. Xubuntu 13.10
The OS X test machine is a 2011 MacBook Pro with 8GB of ram running OS X
10.9
Best
Benedikt
Email Gateway (Aug 19 2022 at 12:40):From: Makarius <makarius@sketis.net>
Another interesting detail here is Windows 8.1. I have recently upgraded
my Windows 8 test machine to 8.1, but made only very brief tests (where it
was looking OK).
Since you also run Linux here: Do you experience differences in the
general performance, running on the same hardware but with quite different
operating systems? This affects Cygwin and Poly/ML running on it.
It is a pending open question if something completely different needs to
be done here, e.g. more native MingW as basis for the Isabelle/ML process.
(Cygwin is required in any case, for add-on tools like E Prover, SPASS
etc.)
Makarius
Email Gateway (Aug 19 2022 at 12:40):From: René Thiemann <rene.thiemann@uibk.ac.at>
Dear all,
I can confirm this.
when proving False via
theory Scratch
imports Main
begin
lemma False
proof (intro TrueE)
the system gets lost somehow (on MacOS X 10.9):
changing the method of (intro TrueE) does not stop the system from evaluation
(comsuming 100% of CPF and eating > 4 GB of RAM)
also if one reloads the buffer, everything remains red and evaluation continues
Here are some more details:
2 x 2.8 Ghz Quad-Core Intel Xeon
6 GB RAM
ML_PLATFORM="x86_64-darwin"
ML_HOME="/Applications/Isabelle2013-2-RC1.app/Isabelle/contrib/polyml-5.5.1-1/x86_64-darwin"
ML_SYSTEM="polyml-5.5.1-1"
ML_OPTIONS="-H 500"
Best regards,
René
Email Gateway (Aug 19 2022 at 12:40):From: bnord <bnord01@gmail.com>
I don't really use this machine a lot for Isabelle development so I
can't give a dependable report here. It maybe feels a little more
responsive under Linux but it's totally fine and maybe it's only my
imagination. But I really don't do much more than browsing theories on
this machine.
Best
Benedikt
Email Gateway (Aug 19 2022 at 12:40):From: Makarius <makarius@sketis.net>
Just another side remark, before I look more closely how Isabelle/Scala
can terminate Isabelle/ML processes more reliably.
Above you are using x86_64-darwin with its unbounded address space,
because polyml-5.5.1 on x86-darwin sometimes cannot allocate heap space
for IsaFoR, as we know already.
The good news is that David Matthews has improved this after the Poly/ML
5.5.1 release, and he will make another release soon.
Then you can also use x86-darwin for your application, which limits the
poly process to comfortable 2-3 GB. This is sufficient in practice, due
to the online sharing of immutable values on the ML heap that David
Matthews is doing for us.
Makarius
Email Gateway (Aug 19 2022 at 12:41):From: Makarius <makarius@sketis.net>
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.
Makarius
Email Gateway (Aug 19 2022 at 12:41):From: bnord <bnord01@gmail.com>
Am 25.11.2013 18:36, schrieb Makarius:
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.
With "recover" I meant that the by(intro TrueE) was again marked as
running and everything worked as expected. I didn't remove the command
or anything.
Just to make sure: the left-over poly process only appeared on Mac OS
X, but not Linux nor Windows?
Yes, I couldn't observe this under Linux nor Windows.
Best
Benedikt
Email Gateway (Aug 19 2022 at 12:41):From: Makarius <makarius@sketis.net>
I have made two more rounds over all this. In the next release candidate
(in 48 hours) it should work better, although there are always situations
where Poly/ML cannot be interrupted quickly. Nonetheless,
interruptibility of Poly/ML is generally better than other platforms I
have seen recently, notably OCaml and JVM.
Makarius
Email Gateway (Aug 19 2022 at 12:42):From: Julian Brunner <julianbrunner@gmail.com>
I just worked with Isabelle/jEdit for a few hours, during which it
became unresponsive about 20 times. The reason for becoming
unresponsive were mostly non-terminating proof methods (mostly force,
blast and auto), although in these cases the non-termination did not
lead to consumption of large amounts of memory like with 'intro
TrueE'. By unresponsive, I mean that it will no longer update the
output panel and the text gets a gray background, which is different
from the regular case of non-terminating proof method which will allow
me to continue working in other places of the document. My system
shows that a poly process takes up one entire CPU core, while not
consuming much memory (just a few hundred MB).
Observations:
removing the non-terminating method invocation by editing the text
does not lead to recovery (at least not within a minute)
closing jEdit terminates all associated processes (including the
non-terminating poly process) almost immediately
it seems like try0 never gets stuck with non-terminating proof
methods, always killing them off after the timeout (for instance,
'apply force' may render the IDE irreversibly unresponsive when
applied to a certain goal, while this is not the case when applying
try0 to the same goal)
I'm running Ubuntu 12.10, x64.
Email Gateway (Aug 19 2022 at 12:43):From: Makarius <makarius@sketis.net>
Thanks for testing.
I can reproduce the problem with Isabelle2013-2-RC1 -- there is still
something utterly wrong with the termination of running tasks. In
Isabelle2013-1 there was too much of it, now there is too little.
Makarius
Last updated: Apr 25 2024 at 04:18 UTC