[isabelle-dev] Regain AFP sanity
Gerwin Klein
gerwin.klein at nicta.com.au
Thu Jan 12 22:09:46 CET 2012
On 13/01/2012, at 2:20 AM, Makarius wrote:
> On Thu, 12 Jan 2012, Gerwin Klein wrote:
>
>> Yes, the default needs to be the full run. That shouldn't be hard to change, though.
>>
>> I'm happy to move the AFP test back to Munich, we'll soon reach saturation on the test server here, and a dedicated machine will give less noise on performance data.
>>
>> Which machine should I run it on?
>
> According to old-style isatest logs (excluding Mira) macbroy2 usually finishes around 05:45. So it could afford a few more hours for AFP (4 or 8 cores, FLYSPECK_SKIP_PROOFS=true).
Ok, I'll do that.
We still need a machine that actually tests Flyspeck, though..
Gerwin
More information about the isabelle-dev
mailing list