[isabelle-dev] AFP/Lifting_Definition_Option

[Ondřej Kunčar]

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.

Bests,
Ondrej

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.
>
> Cheers,
> Gerwin
>
>> 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?
>>
>>
>>        Makarius
>>
>> _______________________________________________
>> isabelle-dev mailing list
>> isabelle-dev at in.tum.de
>> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
>
>
> ________________________________
>
> 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
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
>
tt