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 not empty`.

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 non-empty.

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" tell you?


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