Re: [isabelle] AFP modification policy (was: How to avoid x \<in> carrier G proofs)



Hi Brian,

On 12/12/2010, at 5:02 AM, Brian Huffman wrote:

> On Sat, Dec 11, 2010 at 4:02 AM, Gerwin Klein <gerwin.klein at nicta.com.au> wrote:
>> We give authors access to the development version of the AFP for maintenance, but we trust them to make maintenance changes only and we monitor all commits.
> 
> A "maintenance changes only" policy seems to be at odds with the
> description of this AFP entry:
> 
> http://afp.sourceforge.net/entries/FunWithFunctions.shtml
> 
> Title: 	Fun With Functions
> Author: 	Tobias Nipkow
> Submission date: 	2008-08-26
> Abstract: 	This is a collection of cute puzzles of the form ``Show
> that if a function satisfies the following constraints, it must be
> ...'' Please add further examples to this collection!
> 
> So is it acceptable to add further examples to this entry, or not?

My other email to Joachim hopefully clarifies this already, but the short version for posteriority: it usually will be ok, but only after discussing with the editors and with noting in the public history of the archive.

Tobias' encouragement in the abstract above doesn't mean the added examples should be dropped in silently as maintenance changes. We want them, but we need to know about them. "Normal" people don't have access to the repository, so the question doesn't even arise. They would send in new examples for the collection by email and we can do everything that is necessary. People who have access and could add things themselves only need to let us know about them.

Cheers,
Gerwin




This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.