On 14-07-11 13:07, Makarius wrote:
For the moment, can you try http://www4.in.tum.de/~wenzelm/unofficial/Isabelle_11-Jul-2014.exe with clean default options and settings? It is Isabelle2014-RC0 repackaged with jdk-8u5.
Makarius,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.
Regards, GB ERROR 2ND RUN: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
Description: PNG image