[isabelle-dev] AFP failures near 7f7ca3a43026

[Gerwin Klein]

On 12.06.2014, at 6:11 pm, Jasmin Christian Blanchette <jasmin.blanchette at gmail.com> wrote:

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

No, they don’t. They only do that towards new releases when too many incompatibilities have accumulated and updating entries becomes hard and time consuming. Usually, new entries work fine or are very easily adapted, often before the first test even sees them.

It is actually a very good indicator of how much pain users will be in when they upgrade. In that sense I’m not looking forward to the next release at all (of course there is also a lot of new cool stuff).


> Once this happens, it's easy to miss failures in old entries.

Yes, that is a problem. Maybe the reporting should change to highlight new failures more prominently.


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


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

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.