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 https://cygwin.com/ml/cygwin-announce/2014-05/msg00033.html 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 http://www4.in.tum.de/~wenzelm/unofficial/Isabelle_11-Jul-2014.exe with clean default options and settings? It is Isabelle2014-RC0 repackaged with jdk-8u5.


	Makarius




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