Should we use branches?

[Gerwin Klein]

For seL4 we also have a rebase workflow in git. It’s possible to do in hg, but not as nicely and needs people who know how to deal with it.

Given the problems people get into with just plain hg, I don’t think it would be a good idea for Isabelle or the AFP. It also doesn’t fit with our commit culture on Isabelle ("tuned;"). I would advise against.

I do feel the need to point out that we have long-running branches in our rebase workflow (months, not years, but not daily) — that works perfectly fine if you rebase your branch frequently enough over the trunk, you don’t need to integrate back frequently. But the main benefit of rebase branches is a linear, rational commit history, i.e. a history that is not true but that is the history you would have had if you knew everything in the beginning and wrote the perfect commits. That’s not really the Isabelle model.

There is a lot of benefit in recording the true history as we do in Isabelle, even if that history is less perfect.

Cheers,
Gerwin

On 16 May 2025, at 13:06, Fabian Huch [isabelle-dev-bounces at mailman.proof.cit.tum.de] <forwarded_for at cse.unsw.edu.au> wrote:


The danger of such a model is that branches quickly become stale and a nightmare to rebase. In my experience this model only really works well if developers are well synchronized, so people work on largely distinct pieces of code, or everybody integrates their changes with the trunk frequently, e.g. once per day.

The former doesn't really apply in this environment. The latter one can already do when appropriate, since we have a trunk-based model.

Note that in hg, branches mean divergent lines of work that can't be re-based. What you describe here are topics in hg.


Fabian

On 5/16/25 12:34, Lawrence Paulson via isabelle-dev wrote:
One thing I've noticed at Amazon is that they insist on a single threaded revision trail. They do this by requiring everybody to make their changes within a personal branch, which they then re-base to the main branch before pushing. Sometimes they also merge adjacent commits. In return for mastering a couple of extra commands, everybody benefits from a much cleaner revision history. Do we want to try this?

Larry
<hg.jpeg>

-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20250516/9d0b0fb1/attachment-0001.htm>