Am 12.06.2014 um 10:49 schrieb Gerwin Klein <gerwin.kl...@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 _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
