Re: [isabelle] How to avoid x \<in> carrier G proofs



Hi Joachim,

On 12/12/2010, at 5:10 AM, Joachim Breitner wrote:
> ok, that wasn’t fully clear to me (and I already violated that rule by
> finishing the free-group-isomorphism result in this commit:
> http://afp.hg.sourceforge.net/hgweb/afp/afp/rev/132265dbbf80, sorry for
> that).

I guess the question is what is a "major new theorem" or "major new addition". 

This commit above is ok as an incremental change, and naturally fits into the development entry, so nobody had a problem with it. If you have similar things but just a bit bigger, you should coordinate with the editors, and we're very likely to give you an ok for the change. It should be noted in the public history/changelog of the entry, though.  

Your description sounded like major new work to me, in size at least on the order of the existing entry. I would not say that this is just a small addition or maintenance change then. One indication for this was that you wanted to cite the change. If it's big enough for that, I'd usually think that it is a new entry. It is possible that in some cases (maybe this one too) that it makes sense to merge the new work with an existing entry, and if there are good reasons for it we'll be happy to do that. In any case it at least needs discussion and review, and needs to be marked in the public history of the entry again.

The main concern is that AFP entries need to be citable.  For that to work, it must be clear what a citation refers to, that target must be unchangeable, and it must be reproducible for readers. For an evolving system like Isabelle the last two are in conflict, so we make regular releases and allow maintenance changes. Those that want (convenient) reproducible can download the current version, those that want to know exactly what was described in the paper can download the version that was submitted or cited (a citation will contain the entry name and URL and a year, maybe a month, so that should be clearly defined). 

For this to make sense, even the maintenance version must still at least be close to the cited version. If we accept silent major changes, this breaks.

As evidenced by our discussion, "major" doesn't have a precise meaning and we're happy to be flexible. As a solution to changes that don't warrant a new entry, but that do significantly change what a reader would reasonably expect in an entry, we've introduced a public history/changelog for entries where these changes can be marked and it is made clear for readers what happened when (the version control changelog would be way to low-level for that). As editors we want to know of things that go in there. We haven't had a case yet where we violently disagreed, only cases where we had suggestions for change and usually no problem at all.

So from a practical point of view, we should discuss off-list how big your change really is and if it should be merged or not. It's hard to say without seeing the new development or knowing more about it.


> So at least in this case, I’d like to continue basing my work on
> Isabelle-devel and AFP-devel (otherwise I’d have to undo compatibility
> changes and add all the auxiliary lemmas that went into HOL by now),

This happens from time to time. We can do that, but it has a major disadvantage for you until the next release: you can't really cite the new development yet, even if it is in the afp repository. It only becomes properly visible to site users with the next Isabelle release. The next release is rumoured to be planned for early next year, so this might not be a big deal this time.

The reason it is not citable is that it is not reproducible. It would be major work for a reader or referee to figure out which exact hg id of the entry and of Isabelle you are referring to. It would be hard now, and it would be very hard in 10 years (who knows what version control system we're running then). With just the data of a normal citation it would be pretty much impossible.


> but I’ll not push my changes but rather put my repository somewhere and ask
> the editors to review and merge once (and if) I’m done.


If that is what you want to do, a local hg clone of the afp development repository is probably the right way to go, because you can pull in Isabelle related changes.

Cheers,
Gerwin






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