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



Hi,

This problem makes Isabelle2014-RC0 unusable for me, even for trying to test anything. I attach a screenshot, but I describe the problem a little.

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.

I haven't had a problem like this ever since Isabelle-2012, but I did have file permission problems a long time ago when I was running Isabelle on a USB drive was being used on both XP and Windows 7. Consequently, I know there can be conflicts with file permissions between Cygwin and Windows 7.

What I do different than most people is that I use a Windows user account that doesn't have full admin privileges, and I run Isabelle off of a USB drive that's started with a batch file that sets Cygwin and Isabelle user homes to the same USB drive.

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

Regards,
GB

Attachment: Cygwin_temp_file_prover_process_termination.png
Description: PNG image



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