Re: [isabelle] RC4: sledgehammer on Cygwin crashed once; temp file not removed
On Sat, 23 Aug 2014, Gottfried Barrow wrote:
I got the same failure I was getting with the pre-RC Isabelle2014, but,
for now, it's doesn't appear to be of a catastrophic nature.
I attach a screen shot. It happened when I edited the timeout value.
I've didn't test RC2/RC3, and I've only tested RC4 for several hours, to
see what's up with the new Sledgehammer provers, and provers I haven't
That is one of these hard crashes of the Poly/ML runtime system that
become the more likely the more it approaches certain resource limits.
In the screenshot the sledgehammer invocation has quite a lot of provers.
What is your Multithreading.max_threads_value() in Isabelle/ML?
The question is how many are actuallt run in parellel.
How big is the theory that you were working on?
This archive was generated by a fusion of
Pipermail (Mailman edition) and