[isabelle-dev] AFP failures near 7f7ca3a43026

[Gerwin Klein]

On 12.06.2014, at 7:52 pm, Jasmin Christian Blanchette <jasmin.blanchette at gmail.com> wrote:
>
>> Maybe the reporting should change to highlight new failures more prominently.
>
> Right. Or a "has this entry ever worked" or even a date indicating when the entry last succeeded.

Ok, I'll have a look at implementing this (might take a bit until I get time, though).


>>> The authors/maintainers of the theory would have the freedom to make the entry work at least on their machine, and only then would they be listed for testing.
>>
>> I’d have hoped for a bit more community support than just relying on the author. In fact, the authors are often not in a good position to fix things, because the breakage is entirely related to changes in Isabelle, not to problems in their entry. In this case, we’re lucky.
>
> That's true -- but in the general case where many failures appear at the same time with an unclear origin, I as a member of the community am little enclined to jump in, if for no other reason because I might be duplicating somebody else's work (e.g. Peter's for the CAVA entries).
>
> So here's a new suggestion: When new entries are failing for the first or second time, we should perhaps each time start a mini-thread on isabelle-dev to synchronize on who looks into it. If the author or maintainer intends to look into, he or she should probably just write a short email saying that he will do so; failing this, a developer or AFP editor who is annoyed by the failures could write the first email.

Good point. A little communication will go a long way for this. The initial burden on kicking off the discussion should probably be on the editors, calling for assistance if something is too much to update in the normal submission process.

I still have to look into the current fairly large set of new failures. My guess from a brief look at the log is that something is taking up a large amount of CPU somewhere, triggering timeouts all over the place.

Cheers,
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.