[isabelle-dev] AFP failures near 7f7ca3a43026

[Jasmin Christian Blanchette]

Am 12.06.2014 um 10:49 schrieb Gerwin Klein <gerwin.klein at nicta.com.au>:

>> My suggestion would be not to add the new entries to "ROOT" (or wherever they are listed), so that they are not tested at first.
> 
> I’m very much against that:
> 
> a) it would practically ensure they will never work. Nobody will notice, much less care. Ignoring problems doesn’t make them go away.
> b) it would make ROOTS in development neither a sub set nor a super set of release. For consistency checking, the current super set is very useful.

Good points.

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

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

Jasmin