[isabelle-dev] Library/List_Prefix

[Christian Sternagel]

On 09/03/2012 08:39 PM, Makarius wrote:
> See now Isabelle/7b6beb7e99c1 and AFP/8ad775a1f820.
Thanks!.
> A few more notes to make the process of contributions more and more smooth:
Always welcome.

> 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.
That's clear in principle. What it means for changes to be "applicable 
later" (without causing too many conflicts) is not so clear and may 
heavily depend on the part of the system they concern. For such critical 
(in the sense that conflict potential is high) changes it might be a 
good idea to synchronize with some developer beforehand, such that they 
are almost applied real-time?

> 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).
I can change that on the wiki. Do you think it would be a good idea to 
explicitly mention 'hgext.rebase = '? (But then, I'm not sure what 
happens on a rebase conflict; will resolving such a conflict result in a 
merge node?)

> 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.
What does "unreachable changeset" mean? Is there a good way to modify 
local changesets together with all later ones (in order to correct 
errors; which might be something trivial like a typo in the commit 
message or changes of files that have been committed accidentally by 
forgetting to mention the file-name explicitly in 'hg commit').

> Note that rebasing changes changeset identities -- my later rebasing and your
> earlier rebasing before submitting the bundle.
Just to be clear. Does 'hg pull --rebase' change identities of 
changesets that are pulled or just those of my local changes?

> 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.
Sorry, I forgot about that. What about the attached news.hgbundle?

cheers

chris

-------------- next part --------------
A non-text attachment was scrubbed...
Name: news.hgbundle
Type: application/octet-stream
Size: 1457 bytes
Desc: not available
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20120904/4e405119/attachment-0002.obj>