Email Gateway (Aug 19 2022 at 14:50): Email Gateway (Aug 19 2022 at 14:50):From: Makarius <makarius@sketis.net>
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?
Makarius
Email Gateway (Aug 19 2022 at 14:50):From: Gottfried Barrow <igbi@gmx.com>
It shows "bf5ddf4ec64b".
Regards,
GB
Email Gateway (Aug 19 2022 at 14:50):From: Makarius <makarius@sketis.net>
OK, I will take this as starting point for further investigations.
Do you have any special options? Notably the number of ML threads? The
default is 0 and should give you the real number of CPU cores. You can
check that within a theory document like this:
ML "Multithreading.max_threads_value ()"
What precisely is your version of Windows?
Makarius
Email Gateway (Aug 19 2022 at 14:51):From: Makarius <makarius@sketis.net>
On Fri, 11 Jul 2014, Makarius wrote:
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.
Concerning the "Isabelle/HOL too big to fail" hypothesis: you can try to
give a bit more ML heap, to make it feel more comfortably.
The Isabelle/jEdit file browser now has Favourites for $ISABELLE_HOME_USER
-- go there and open the file etc/settings (which probably does not exist
yet); then add the following settings line:
ML_OPTIONS="-H 1000"
The default for that is 500.
I've been using Isabelle_28-May-2014 for about 2 or 3 weeks and
haven't had this problem.
Looking closely at this Isabelle/bf5ddf4ec64b I see very few significant
differences. The bundled Poly/ML is exactly the same version 5.5.2, which
means there is nothing to see there.
There are two main changes between Isabelle_28-May-2014 and
Isabelle2014-RC0:
* from experimental jdk-8u5 back to stable jdk-7u60
* update to Cygwin 1.7.30-1
Cygwin has a form of "rolling releases", so there is always some risk to
shoot at it blindly. The announcement
https://cygwin.com/ml/cygwin-announce/2014-05/msg00033.html looked like it
would be an improvement, but when Corinna Vinschen says "This is a bugfix
release" it could also mean there are new attempts to address old
problems, without solving them.
I will experiment further with Cygwin variants after VSL next week.
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
Email Gateway (Aug 19 2022 at 14:51):From: Gottfried Barrow <igbi@gmx.com>
I put 'ML_OPTIONS="-H 1000" ' in my user etc file and it makes no
difference.
I'll run Isabelle_11-Jul-2014.exe with the default options, but it's
possible I'll ride my bicycle first, thinking about Andre Greipel and
Marcel Kittel, and how they've dished up a lot of humble pie the last
few years to that guy who crashed out. Where's the dissing of Greipel
now, that he's free to compete? Nice guys, who win.
Regards,
GB
Email Gateway (Aug 19 2022 at 14:51):From: Gottfried Barrow <igbi@gmx.com>
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
Isabelle_11-Jul-2014_process_terminate.png
Email Gateway (Aug 19 2022 at 15:19):From: Gottfried Barrow <igbi@gmx.com>
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
Cygwin_temp_file_prover_process_termination.png
Last updated: Apr 23 2024 at 16:19 UTC