[isabelle-dev] Publishing contributions as an external

Alexander Krauss krauss at in.tum.de
Mon Apr 16 21:21:08 CEST 2012


On 04/16/2012 11:52 AM, Makarius wrote:

>> @Lukas: Thanks for pointing me to "mercurial queues" which are really
>> a great tool. Using queues it should be easily possible (even as an
>> external) to avoid the long "pilage" of private changes and public
>> commits.
>
> The queues became quite popular early for Isabelle/Mercurial experts. So
> far I've never tried it myself.
>
> I wonder if the more recent rebase extension would do similar things in
> a more basic way. Are there any users of it?

Yes. For the occasional rebasing, the rebase extension is better. 
Moreover, the patch queue working model breaks down when you get 
complicated merges (basically you then get patches that won't apply any 
longer, and are thrown back to merge manually (unless you use further 
extensions, IIRC)). But patch queues have other advantages...

In very recent Mercurials, there is also the "hg graft" command, which 
has a similar purpose but is part of the core.

The bottom line is that you need some form of rebasing for anything that 
you do not manage to "serve while it is hot". How you do it is up to you.

I personally violate the "don't keep changes private" principle 
considerably: I have a few patches lying around that are more than a 
year old. This is not a problem as such, as long as I rebase finally 
before I push, but it brings some overhead.

A completely different question is whether we can open testboard to 
externals. This might reduce some communication overhead we are seeing 
at the moment ("I'm currently testing...", "I have pushed...", etc.)
Essentially, this is just a matter of setting up a proper push-via-https 
repository and managing a list of authorized people (we cannot make 
testboard completely open since we execute code that is pushed there. 
But it should be ok to give access to people known to us).

Alex



More information about the isabelle-dev mailing list