Re: [isabelle] Isabelle2013-RC2 available for testing

On Mon, 28 Jan 2013, Gottfried Barrow wrote:

So Sledgehammer is back in the saddle again. I run 13 ATPs together, and the ATPs that normally find proofs all return normally. If I run 24 ATPs together, then it seems to cause some of the ATPs to time out or terminate when they otherwise wouldn't, but they terminate in a normal manner by returning an error message.

It should actually work better than in Isabelle2012 now. It was just an accident that the Cygwin version from that time was handling the inherently fragile spawing of external processes most of the time. The Cygwin in Isabelle2013-RC1 was less benign, and this old problem was harder to ignore.

For Isabelle2013-RC2, David Matthews changed Poly/ML to work with parallel Cygwin processes in a robust manner. I managed to run tests like HOL-Nitpick_Example with all its Java processes for Kodkod without problems.

If anybody still sees external Cygwin processes that crash in strange ways (with stack dump), or left-over processes that are not cancelled properly, please report this. (You can use the Windows task manager or "ps" on the Cygwin Terminal to check this.)


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