Re: [isabelle] Parallel proofs issue, potentially in subst method



On Thu, 13 Sep 2012, Gerwin Klein wrote:

On 13/09/2012, at 4:16 AM, Makarius <makarius at sketis.net> wrote:
On Mon, 10 Sep 2012, Rafal Kolanski wrote:

I have recently come across an issue when trying to improve the runtimes of our regression test server. When I ran it with -q 1, the times improved drastically, which was nice. When I ran it with -q 2 though, it didn't build at all.

Now the world knows that the top-secret proofs of L4.verified are still checked sequentially :-)

Imagine the pain we've been in all that time ;-)

It is also a natural consequence of disclosed sources, but you know this already.


	Makarius





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