[isabelle-dev] Library/List_Prefix

[Makarius]

On Tue, 4 Sep 2012, Christian Sternagel wrote:

> 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?

"Applicable later" is defined semantically, but you have already named 
some syntactic criteria for it.  The areas of activity in the source tree 
are distributed quite unevenly.  After time one gets a feeling what is 
feasible and what not.  There used to be classic hotspots for conflicts, 
like src/HOL/IsaMakefile, but that is now an episode of the past.  Files 
like src/HOL/ROOT are intentionally written in a manner such that 
line-based merges become trivial and usually conflict-free.

In general the development model on the repository is concurrent and 
lock-free.  So you don't make a broadcast announcement like "everbody wait 
until I have finished working here or there".  It is just too combersome 
and not very efficient.  It is also semantically against the usual 
Isabelle development attitudes, because realistically you don't know in 
advance how long a certain change will take to get right when starting 
thinking and editing.


BTW, the term "developer" is now used in many projects in the sense of 
someone who produces changesets and passes them somewhere else, usually 
towards some "maintainer" who is rebasing or merging things, to hand them 
on further.

I am myself a jEdit developer in the sense, because I have occasionally 
submitted (informal) diffs to one of the many trackers of that project.


>> 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?

Yes.  This seems to be a relatively new addition to Mercurial from Git 
space, where people rewrite historical all the time.

A practical consequence of the delayed submission model, with rebase by 
the maintainer on the other end seems to be that you cannot easily quote 
other changesets of your current queue.  But quoting usually indicates 
amendment of changesets that were not right in the first place.  A small 
linear clean chain of changes can usually stand on their own, without 
internal pointers.

As long as a certain chain of changesets has not been published yet, it 
might be better to use Mercurial queues to put them into shape.  (I am 
myself not an expert on that.)  Some of the newer front-ends also allow to 
"amend" unpublished changesets by applying some non-monotonic operations 
behind the scenes.


>> 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?

I have pushed that here: Isabelle/0ee5983e3d59.


 	Makarius