makarius at sketis.net
Fri Sep 7 16:32:25 CEST 2012
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
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
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.
More information about the isabelle-dev