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 normally used.

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?


	Makarius




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