[isabelle-dev] AFP failures near 7f7ca3a43026

[Jasmin Christian Blanchette]

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

> In the first instance, it is the authors/maintainers of the entry that we will ask for help. In this case, Peter has promised to look at this set of new entries (CAVA etc), but it will take him some time.
> 
> We usually have this state of affairs close to new Isabelle releases when too many incompatibilities have accumulated. I don’t have a good solution either, but I’m open to ideas.

I don't know or understand much the AFP submission process, but from my point of view the issue is that tests (whether nightly tests or those run automatically on the repository or testboard) report failures whenever new entries are added. Once this happens, it's easy to miss failures in old entries.

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

Jasmin