Re: [isabelle] Isabelle2013-RC1 Sledge output finicky



On Fri, 25 Jan 2013, Makarius wrote:

On Thu, 24 Jan 2013, Gottfried Barrow wrote:

In general, the ATPs are only working if they're run by themselves.

I can confirm that in both in Isabelle2012 and Isabelle2013-RC1 executing many processes in parallel on Windows/Cygwin is very fragile. It seems to have been always like that, but only with Isabelle2012 we could speak of reasonably Windows support in the first place. Now that so many other thinks are working better than before, such drop-outs become more apparent.

Let's see if we can figure out a solution to the problem ...

In the meantime David Matthews, who is the master behind Poly/ML, managed to work around the problem with Cygwin and multithreaded execution of external processes.

Once his change shows up officially on his polyml-code/fixes-5.5 branch, I will repackage it for Isabelle and produce Isabelle2013-RC2.

In the history of Isabelle on Windows, this will be the first time where all regular test sessions are running through, even HOL-Nitpick_Examples with its many externaly Java processes.

Stay tuned and keep fingers crossed ...


	Makarius






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