[isabelle-dev] AFP devel broken

[Gerwin Klein]

On 06/12/2012, at 9:25 PM, Johannes Hölzl <hoelzl at in.tum.de> wrote:

> Am Mittwoch, den 05.12.2012, 21:50 +0000 schrieb Gerwin Klein:
>> On 05/12/2012, at 6:31 PM, Tobias Nipkow <nipkow at in.tum.de> wrote:
>>
>>> Can anybody still build the AFP on some machine?
>>
>> I have been able to build everything on a linux machine late last
>> night.
>>
>> The only entry that comes up with an error is Girth_Cromatic
>> (something with filter_lim that looks related to a recent change).
>
> This is fixed in changeset AFP/7d05a06f8793. I did the commit 2 days
> ago, but maybe I forgot to push it.

I can confirm now that it works with AFP/7d05a06f8793 and Isabelle/52d9720f7a48.

So the good news is that all AFP entries currently work.

The bad news is that I just had the session hanging on our Linux server with fast local SSD (I killed HOL-Multivariate_Analysis after 44min on 0% CPU). Still no real idea what's going on.

Could it be something to do with document, browser_info, and document_variant options? These are the only settings that seem different to mira and other isatest runs.

Gerwin

________________________________

The information in this e-mail may be confidential and subject to legal professional privilege and/or copyright. National ICT Australia Limited accepts no liability for any damage caused by this email or its attachments.