Email Gateway (May 16 2025 at 10:44): Email Gateway (May 16 2025 at 10:44):From: Lawrence Paulson via isabelle-dev <isabelle-dev@mailman.proof.cit.tum.de>
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
[cid:6ce32522-80e2-4611-8cd1-3eecd6e69d1d@GBRP265.PROD.OUTLOOK.COM]
Email Gateway (May 16 2025 at 11:06):From: Fabian Huch <huch@in.tum.de>
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
Email Gateway (May 16 2025 at 11:13):From: Lawrence Paulson via isabelle-dev <isabelle-dev@mailman.proof.cit.tum.de>
Thanks for the correction regarding topics in hg.
My impression is that developers do rebase daily in order to avoid merge issues. Of course, these rebase steps leave no trace in the commit history, and there are no visible merges either.
Larry
On 16 May 2025, at 12:06, Fabian Huch <huch@in.tum.de> 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.
Email Gateway (May 16 2025 at 11:23):From: Gerwin Klein via isabelle-dev <isabelle-dev@mailman.proof.cit.tum.de>
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@mailman.proof.cit.tum.de] <forwarded_for@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>
Email Gateway (May 16 2025 at 11:28):From: Fabian Huch <huch@in.tum.de>
On 5/16/25 13:22, Gerwin Klein via isabelle-dev wrote:
It’s possible to do in hg, but not as nicely
Actually I find it much easier to do such operations in hg: Because it
allows you to simply talk about changesets, all the operations and
commands get a lot easier (especially for beginners!).
E.g. to rebase one commit onto another you just do
hg rebase --source xxx --dest yyy
And the histedit extension allows you to do a lot more operations with
ease as well.
and needs people who know how to deal with it.
That's certainly a problem.
Fabian
Email Gateway (May 16 2025 at 12:15):From: Makarius <makarius@sketis.net>
On 16/05/2025 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?
No.
Isabelle has a much better culture than most projects out there.
See also README_REPOSITORY.
Makarius
Email Gateway (May 16 2025 at 12:18):From: Makarius <makarius@sketis.net>
On 16/05/2025 13:22, Gerwin Klein via isabelle-dev wrote:
There is a lot of benefit in recording the true history as we do in Isabelle,
even if that history is less perfect.
True history is very important. I would call that more perfect than a history
that is manipulated to "look better".
Makarius
Last updated: May 31 2025 at 01:44 UTC