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:
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
* 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
clean default options and settings? It is Isabelle2014-RC0 repackaged
This archive was generated by a fusion of
Pipermail (Mailman edition) and