[isabelle-dev] Library/List_Prefix

[Makarius]

On Mon, 3 Sep 2012, Christian Sternagel wrote:

> On 09/03/2012 08:29 AM, Gerwin Klein wrote:
>> You attached a patch, but I'm not sure anyone feels responsible for pushing 
>> it ;-)
>> 
>> Have you been working on this with someone from Munich?
> No, against my own advice ( 
> https://isabelle.in.tum.de/community/Publish_contributions_as_an_external ) I 
> haven't.
>
> The reply that got me going was the rather noncommittal:

See now Isabelle/7b6beb7e99c1 and AFP/8ad775a1f820.

A few more notes to make the process of contributions more and more 
smooth:

There is no real-time reactivity on isabelle-dev, so your changes should 
not be expected to be applied immediately, and then only after some 
moderation.

This means it does not make sense to publish merge nodes (you did not have 
any, but merge is still mentioned on 
https://isabelle.in.tum.de/community/Main_Page).

Submitted changes should be easy to import and/or rebase, which was the 
mainly case here, apart from what is Isabelle/0da7116b1b23 and 
Isabelle/6be57c7d84f8 now -- they refer to unreachable changesets.  Note 
that rebasing changes changeset identities -- my later rebasing and your 
earlier rebasing before submitting the bundle.

We still need a few lines of NEWS and CONTRIBUTORS.  The NEWS are the 
final proof that a change is "user-relevant" -- Why do it in the first 
place if it is not? Moreover, the NEWS should contain a few lines of 
summary of your experience with porting Isabelle applications and AFP, 
i.e. the infamous INCOMPATIBILITY as the bad news.


 	Makarius