[isabelle-dev] Regain AFP sanity

Gerwin Klein gerwin.klein at nicta.com.au
Wed Jan 18 22:42:07 CET 2012


Ok, no use in providing additional heating at TUM, I guess.

I'll set it up such that it runs the full test once a week and the reduced version daily.

Gerwin

On 19/01/2012, at 8:25 AM, Tobias Nipkow wrote:

> Yes, this is a very reasonable test.
> 
> Tobias
> 
> Am 18/01/2012 21:55, schrieb Makarius:
>> BTW, this versions merely skips the really slow proofs of same4, same5,
>> same6, but runs the fast one of same3 unconditionally.  Superficially
>> this looks like a reasonable test.  Or is their significant information
>> gained from attempting the slow proofs as well (say once a week or once
>> a month)? Tobias should be able to say more about it.
>> 
>> 
>>    Makarius
>> _______________________________________________
>> isabelle-dev mailing list
>> isabelle-dev at in.tum.de
>> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
> _______________________________________________
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
> 




More information about the isabelle-dev mailing list