Re: [isabelle] RC4: sledgehammer on Cygwin crashed once; temp file not removed



On 14-08-26 04:05, Makarius wrote:
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?

The theory is not that big, about 1700 lines, which takes about 8 seconds to prove.

I was just starting with RC4, so I think threads was set by the default "0" in the options, which appears to give me 4 threads, since I have an older quad core.

I've been running with the thread options set to 4, and it has only crashed that one time, and I've now been running sledgehammer quite a bit over 6 hours or so.

For observational purposes, I have the "sledgehammer_params" set to use 17 provers, and I also have those 17 in the "Provers" option for the Sledgehammer panel.

I list the 17 below and I've set threads=12 now, and, watching the number of processes, it appears willing to actually start the number of threads that max_threads_value() is set to.

For the first provers in the list, I interleave local provers with remote provers, with the best 3 locals at the beginning, z3, e, and spass, and I think it starts all the provers in the order listed. So, with threads=4, remote_spass_pirate wasn't returning with an error quickly, but with threads=12, it was failing after a few seconds, for a particular proof.

Provers:

z3 remote_vampire e remote_e_tofof spass remote_iprover remote_snark remote_e_sine remote_iprover_eq agsyhol remote_spass_pirate satallax remote_waldmeister_new leo2 remote_satallax remote_agsyhol remote_leo2

The short story is that RC0 and RC4 have failed in a way that Cygwin Isabelle hasn't failed before, so something has changed. RC4 has only failed once, so it could be a rare thing.

On the surface, Isabelle2014 doesn't seem to be a big change, though I suppose that's because I've already been exposed to it a while, such as to datatype_new.

There is one huge surface addition, and that's \<open> and \<closed>. Those are huge, because they're subtle and graphical, and they help to clearly delimit the beginning and end of text, better than {* and *}, though those have their use.

In watching Sledgehammer with "verbose=true", it also appears that machine learning is in the house. The prover "e" has become very competitive with remote_vampire.

Regards,
GB









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