Christian Doczkal (Jun 17 2020 at 13:06): Christian Doczkal (Jun 17 2020 at 13:06):I noticed that pull requests frequently get the "needs: rebase" tag, even though conflicts are limited to CHANGELOG_UNRELEASED.md. Conflicts in this file are something one might want to resolve (by hand) when merging, given that essentially every PR touches this file. Moreover, it might be desirable on to run the CI pipeline on the generated merge commit, even if there is a conflict in the change log. Would this be technically feasible with the tools provided by GitHub? Would this be desirable?
Théo Zimmermann (Jun 17 2020 at 13:14):Yes, it would be technically feasible since it is the bot who attempts to do a merge before running CI. We could adopt any kind of automatic resolution strategy for this file since it is irrelevant for CI. Please open an issue on the bot's repository if you'd like that: https://github.com/coq/bot. We could also discuss this further in the bot's Zulip stream.
Enrico Tassi (Jun 17 2020 at 13:15):FTR in MC we merge with GH button, and this gives you a very basic text editor to solve these conflicts. So I supposed it would be enough to be able to pass to coqbot a list of file for which conflicts should be ignored.
Enrico Tassi (Jun 17 2020 at 13:16):I mean, no real AI seems needed here
Théo Zimmermann (Jun 17 2020 at 13:16):But maybe if conflicts in this file are that frequent, it means that it is time to adopt a different strategy for the unreleased changelog à la GitLab / Coq. Cf. https://about.gitlab.com/blog/2018/07/03/solving-gitlabs-changelog-conflict-crisis/ and my thesis, sections 5.5.2 and 5.5.3.
Théo Zimmermann (Jun 17 2020 at 13:17):Enrico Tassi said:
FTR in MC we merge with GH button, and this gives you a very basic text editor to solve these conflicts. So I supposed it would be enough to be able to pass to coqbot a list of file for which conflicts should be ignored.
Yep, that sounds reasonable.
Théo Zimmermann (Jun 17 2020 at 13:17):By "automatic resolution strategy", I just meant: use the base branch version or something like that.
Christian Doczkal (Jun 17 2020 at 13:35):If I understand the aforementioned blog post correctly, the general idea is to have a directory for "unreleased changes" and to aggregate those when tagging a release. If there is tool support in order to not burden the release managers, then I would consider this preferable to the coqbot based approach. @Enrico Tassi , what do you think? (I'm not familiar with how this is handled on the Coq side)
Enrico Tassi (Jun 17 2020 at 13:43):if you follow a strict naming schema, then it can be as simple as (echo Version $V $DATE; cat changelog.d/* changelog.md) > changelog.new; rm changelog.d/*. In Coq the Changelog is part of the manual, it's the sphinx scripts that glues the files.
Enrico Tassi (Jun 17 2020 at 13:46):My personal opinion is that CI should not be skipped for conflicts on the changelog (no matter which format you pick), and I like to see the changelog as a document you write, possibly step by step, but definitely not byproduct of git log. In my (small) project I keep a file, and I work on it as I work on the README.
Enrico Tassi (Jun 17 2020 at 13:47):1 file per PR mentioning the PR, the author and a line of text is a byproduct of git log, IMO.
Enrico Tassi (Jun 17 2020 at 13:49):And having it "automatically generated" makes it hard to edit it before the release day. But this is just my opinion, and it is not a strong one. I agree it should not get in the way, but here the problems seems that CI/Coqbot is too simple, not that we get real hard to solve conflicts in the file.
Cyril Cohen (Jun 17 2020 at 14:29):I think agree with @Enrico Tassi here, I think we want to make sure the changelog is globally edited by humans for every PR: it happened several times to me that we could amend, improve, refactor or even sometimes retract previous bullets of the changelog in one PR, so each PR having its own changelog defeats that purpose. Moreover we do not have a policy of backporting changes yet... (if we do that might change everything because indeed changelog entries can only be relocatable if they have their own file).
That being said, these conflicts are getting on my nerve too. I like the CI ignoring merge conflicts in non program (i.e. basically non *.v, Make* or _CoqProject) files for mathcomp. I am also wondering if we could have an improved merge script that would be cleverer in solving bullet adding only changelog conflicts. Maybe using the prefilled dashed with enough dashes trick :laughing: and if we feel the need for more, we evolve, incrementally. I don't know...
Théo Zimmermann (Jun 17 2020 at 15:49):Note that the many dashes trick is also a strategy that was used by GitLab at some point :wink:
Cyril Cohen (Jun 17 2020 at 15:54):Judging by the README, this looks nice: http://git.savannah.gnu.org/gitweb/?p=gnulib.git;a=blob;f=lib/git-merge-changelog.c
Cyril Cohen (Aug 11 2020 at 02:03):FTR I just merged https://github.com/math-comp/math-comp/pull/551.
It does not solve conflicts on github yet (cf https://github.com/isaacs/github/issues/487 and https://github.com/isaacs/github/issues/560, so it's likely to be supported in the future, given gitlab does... hopefully).
However, locally, I tested it on a few git rebase that would conflict, and it does not anymore. :tada: :tada:
Last updated: Nov 29 2023 at 19:01 UTC