Gerwin.Klein at nicta.com.au
Thu Oct 8 00:09:38 CEST 2015
The second option has happened now.
> On 8 Oct 2015, at 1:08 am, Ondřej Kunčar <kuncar at in.tum.de> wrote:
> This is what I already did when I pushed the upgrade of the lifting package. I contacted René Thiemann and proposed to make his AFP entry empty except for a single file that would explain what happened.
> As far as I can remember, he wasn't happy with this solution and proposed to keep the entry and put the information that this entry is superseded by something else in the description of the entry.
> I can see now that even this didn't happen: I guess I assumed that René would do it and he assumed that I would do it. This is my fault. I should have made this assumption clearer.
> On 10/05/2015 11:33 PM, Gerwin Klein wrote:
>> The first step would be to contact the authors of the entry.
>> If they agree that it is superseded by something else, the entry can be made empty, with an explanation/referral to whatever replaced it.
>>> On 06.10.2015, at 03:15, Makarius <makarius at sketis.net> wrote:
>>> What is the purpose of AFP/Lifting_Definition_Option? Isn't that already superseded by an upgrade of the regular lifting package?
>>> I've come across a broken AFP/Lifting_Definition_Option several times, and then spent extra time to maintain it, wondering if this is just dead code anyway.
>>> Is there a procedure to remove obsolete material from the AFP?
>>> isabelle-dev mailing list
>>> isabelle-dev at in.tum.de
>> 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.
>> isabelle-dev mailing list
>> isabelle-dev at in.tum.de
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
More information about the isabelle-dev