Externally merged commits are not marked as merged

[AdamMajer]

Description

1. create repo
2. create fork
3. do channge and create PR to repo
4. merge manually with git merge --ff-only ... as per instructions
5. PR not marked as merged, just says the commit already there and nothing to do.

Gitea Version

1.22 , or demo site

Can you reproduce the bug on the Gitea demo site?

Yes

Log Gist

No response

Screenshots

from: https://demo.gitea.com/gnuman/test/pulls/1

THEN I added another commit, and it got added to the PR (I guess since it wasn't closed) and the instructions are different from above. Maybe above it reverted to default ones? But this could be another issue not related to this one.

Git Version

No response

Operating System

No response

How are you running Gitea?

demo site

Database

None

[wxiaoguang]

Workaround: you could enable "Manually Merge" in the repo settings, and manually merge it.

---

ps: not sure whether it is a regression, I never used that workflow 🤔 is there any further information to confirm whether it is a regression?

[AdamMajer]

Manual merge is a workaround, I think.

If I'm following the command-line instructions, gitea should be smart enough to notice that the commits are there in the branch already, and close it as merged. The logic is simply, on push to target branch, if "all commits exist in the target branch, so it's merged, mark as done".

Is there a common use-case when this is not desired?

[AdamMajer]

You are correct, maybe this is not a regression. It just maybe never worked.

[delvh]

Is there a common use-case when this is not desired?

performance. And no one implemented it so far.
But I do think it is non-trivial to find all PRs that can be closed once you push:
You need to find all PRs that target the branch you push to.
On top of that, you then need to ensure that all commits are contained within your branch - the only way to do this reliably is by asking Git on every matching PR individually if there are diverging commits.
You cannot just do a DB lookup as then the case you merged the branch locally and added a commit on top before pushing is not covered (although that is a rare edge case)

The moment you have a repo with lots of open PRs, I can predict that pushing will take forever, especially if your hardware isn't the strongest.
However, the performance problem could be solved by adding a instance-wide setting that toggles this behavior.

[AdamMajer]

Well, you only need to check the if the commit id of PR head is in the target branch, nothing else.. If that is the case, then it's merged. IFF the PR head commit id is in the branch head, then the PR is FF merged.

You cannot just do a DB lookup as then the case you merged the branch locally and added a commit on top before pushing is not covered (although that is a rare edge case)

As long as the commit id from PR head is there, it has to be merged. Other things on-top, well, maybe extra commits? But that is a different discussion, I think.

What has to be done is, for all pushes to target repo, check all open PR if the commit id is in the repo, if yes, mark as merged. Nothing more to do.

If no one does this, I'll try to get to it next week.

[delvh]

Well, you only need to check the if the commit id of PR head is in the target branch, nothing else.

Yes, but you first need to find all applicable PRs and do this git call for all of them separately, so that point still stands.
But sure, go ahead, I'll review your PR dutifully once it exists.
(If I forget to, ping me. Unfortunately, my TODO list is so long that I frequently forget what I wanted to do)

[a1012112796]

I has try a new solution in #21951 . which try add a new push option to notify server that a pull request was merged in this push operation (example git push -o pulls.merged=1,2,3 -u origin master). I think it would be a better way.

[a1012112796]

if "all commits exist in the target branch, so it's merged, mark as done".
? Is there a common use-case when this is not desired?

Because empty pull request has been allowed in #12543

[AdamMajer]

Well, the idea here is if a PR head commit ID is present in the new push to the target branch, then it's merged. Nothing else needed.

This of course will not detect anything when the commit is altered in any way because then the commit ID will be changed. Another solution would then be required for those workflows. The push option looks like it would be helpful in those cases.

[AdamMajer]

I don't quite understand the point of empty PR. It seems they would just be issues. But empty PR are not the same as a PR with a HEAD commit ID present in a push to target branch. Or am I misunderstanding this?