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



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 ;-)

We can now do this, because we have a regression test server with 128GB RAM.

My desktop machine still needs to run sessions sequentially to get things through, although poly 5.5.0 has made the situation dramatically better.

Cheers,
Gerwin






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