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
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 ...
This archive was generated by a fusion of
Pipermail (Mailman edition) and