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

On 14-07-11 13:07, Makarius wrote:
For the moment, can you try with clean default options and settings? It is Isabelle2014-RC0 repackaged with jdk-8u5.


It does the same thing. I attach a screenshot that shows the first run. Sledgehammer ran, then completed, then the prover terminated.

After closing and restarting and doing it again, it then gives the error message about "rmdir" and "tmp", as shown below.

I let it install to my desktop and didn't make any option changes, and I installed "Isabelle2014-RC0.exe" under my Win7 admin account. The error is consistent.

When trying Sledgehammer on a simple theorem it doesn't get an error. I get the error when trying Sledgehammer on previous proof steps that I had actually used Sledgehammer to get a proof.



Unofficial version of Isabelle/HOL (Isabelle repository snapshot 6c18c6418b99 11-Jul-2014)
rmdir: failed to remove `/tmp/isabelle-jv3512': Directory not empty

standard_output terminated
standard_error terminated
process terminated
command_input terminated
Cannot read message:
Socket closed
message_output terminated
process_manager terminated
Return code: 0

Attachment: Isabelle_11-Jul-2014_process_terminate.png
Description: PNG image

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