Re: [isabelle] Isabelle2014-RC0: Cygwin can't delete temp files, the prover terminates
On Wed, 9 Jul 2014, Gottfried Barrow wrote:
After having gotten this type of error with Isabelle2014-RC0 when
running Sledgehammer, I started Sledgehammer, then I started to edit the
Sledgehammer command to simplify it, but, before finishing my edit, I
got the message "rmdir: failed to remove `/tmp/isabelle-1252`: Directory
That describes the basic problem. The prover runs Sledgehammer, but at
some point, after it starts to try and delete its temp files, it can't,
and the prover process is terminated.
The causility is the opposite: the ML process has crashed and left some
tmp files behind, so the tmp directory was not removed, because it was
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.
I've been using Isabelle_28-May-2014 for about 2 or 3 weeks and haven't
had this problem.
The label 28-May-2014 does not have any official status to identify that
version -- I need the Mercurial hash key.
Using the Cygwin Terminal of that version, what does "isabelle version -i"
This archive was generated by a fusion of
Pipermail (Mailman edition) and