[isabelle-dev] [isabelle] HOLCF equality

[Lawrence Paulson]

I would say that this discussion is better confined to the developers' list.

Entries need to be maintained. This surely includes extending them and streamlining existing proofs. It surely does not include replacing a development by entirely different development with related objectives. I don't think that the AFP should guarantee upwards compatibility for the sake of people who have decided to take a AFP entry as a starting point their own development. And I don't think we want AFP entries to become like Wikipedia articles that anybody could edit (and that would require continual policing).

A Wikipedia of proofs (including automatic checks to ensure that the proofs are sound) might be an interesting experiment, but I doubt that there are enough users out there skills and time needed even to run such an experiment.

Larry

On 9 Jul 2012, at 22:00, Makarius wrote:

> On Mon, 9 Jul 2012, Tobias Nipkow wrote:
> 
>> Am 09/07/2012 15:04, schrieb Brian Huffman:
>>> Maybe using the distribution is better; as an "archive", the AFP seems not to be intended so much for dynamic, growing works with open authorship.
>> 
>> The distribution is more lightweight than the AFP. But in either case the set of people that can add contributions will be restricted.
> 
> After several successful years of AFP, this question is still coming up routinely, and I wonder myself often.
> 
> Can the official AFP editors make some more explicit statements on the AFP website what it really is?  What are the official policies to grow it? Will new versions of articles replace old ones, keeping the name or changing the name? Etc. etc.
> 
> For example, JinjaThreads seems to have been a perfectly dynamic entry in all these years, without any archival character beyond the Mercurial history.
> 
> 
> 	Makarius
>