Re: [isabelle] Isabelle2014-RC0: Cygwin can't delete temp files, the prover terminates

On Fri, 11 Jul 2014, Makarius wrote:

We need to figure out why the process failed so badly. Maybe Isabelle/HOL is now too big for the defaults from the past, such that it hits a concrete wall more often.

Concerning the "Isabelle/HOL too big to fail" hypothesis: you can try to give a bit more ML heap, to make it feel more comfortably.

The Isabelle/jEdit file browser now has Favourites for $ISABELLE_HOME_USER -- go there and open the file etc/settings (which probably does not exist yet); then add the following settings line:

ML_OPTIONS="-H 1000"

The default for that is 500.

 I've been using Isabelle_28-May-2014 for about 2 or 3 weeks and
 haven't had this problem.

Looking closely at this Isabelle/bf5ddf4ec64b I see very few significant differences. The bundled Poly/ML is exactly the same version 5.5.2, which means there is nothing to see there.

There are two main changes between Isabelle_28-May-2014 and Isabelle2014-RC0:

  * from experimental jdk-8u5 back to stable jdk-7u60

  * update to Cygwin 1.7.30-1

Cygwin has a form of "rolling releases", so there is always some risk to shoot at it blindly. The announcement looked like it would be an improvement, but when Corinna Vinschen says "This is a bugfix release" it could also mean there are new attempts to address old problems, without solving them.

I will experiment further with Cygwin variants after VSL next week.

For the moment, can you try with clean default options and settings? It is Isabelle2014-RC0 repackaged with jdk-8u5.


This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.