Stream: coqbot devs & users

Topic: coqbot merge now issue


view this post on Zulip Théo Zimmermann (Oct 18 2022 at 16:12):

The issue reported by Michael in https://github.com/coq/coq/pull/16688 corresponds to the following in the log:

Error while merging PR: Json type error: Can't get member 'mergePullRequest' of non-object type null. Body was:
{"errors":[{"message":"Something went wrong while executing your query. Please include `C000:3BF3:351C9DC:6CA68DF:634ECC7A` when reporting this issue."}]}. Request was:
{"query":"mutation mergePullRequest($pr_id: ID!, $commit_headline: String, $commit_body: String, $merge_method: PullRequestMergeMethod) {\nmergePullRequest(input: {pullRequestId: $pr_id, commitHeadline: $commit_headline, commitBody: $commit_body, mergeMethod: $merge_method}) {\npullRequest {\nmerged \nmergedAt \nstate \nurl \n}\n\n}\n\n}\n","variables":{"pr_id":"PR_kwDOABUDh85A8UqR","commit_headline":"Merge PR #16688: Windows CI: use coq-ci branch from Platform.","commit_body":"Reviewed-by: MSoegtropIMC\nCo-authored-by: MSoegtropIMC <MSoegtropIMC@users.noreply.github.com>\n","merge_method":"MERGE"}}

Said otherwise, the query was:

mutation mergePullRequest($pr_id: ID!, $commit_headline: String, $commit_body: String, $merge_method: PullRequestMergeMethod) {
  mergePullRequest(input: {pullRequestId: $pr_id, commitHeadline: $commit_headline, commitBody: $commit_body, mergeMethod: $merge_method}) {
    pullRequest {
      merged
      mergedAt
      state
      url
    }
  }
}

With variables:

{"pr_id":"PR_kwDOABUDh85A8UqR",
"commit_headline":"Merge PR #16688: Windows CI: use coq-ci branch from Platform.",
"commit_body":"Reviewed-by: MSoegtropIMC\nCo-authored-by: MSoegtropIMC <MSoegtropIMC@users.noreply.github.com>\n",
"merge_method":"MERGE"}

view this post on Zulip Théo Zimmermann (Oct 18 2022 at 16:56):

@Michael Soegtrop Would you mind doing a test for me?
You should go to https://docs.github.com/en/graphql/overview/explorer, log in with your GitHub account, and execute the above request (copy the query part in the first text field and the variable part in the second text field).
I would do it myself, but that would give the impression that I'm merging my own PRs if that works.

view this post on Zulip Michael Soegtrop (Oct 19 2022 at 07:34):

@Théo Zimmermann : I get this response:

{
  "errors": [
    {
      "message": "Something went wrong while executing your query. Please include `1456:2C40:3490D1:6CB29D:634FA841` when reporting this issue."
    }
  ]
}

view this post on Zulip Théo Zimmermann (Oct 19 2022 at 07:40):

Thanks @Michael Soegtrop, can you try again, but this time with:

mutation mergePullRequest($pr_id: ID!, $commit_headline: String, $commit_body: String) {
  mergePullRequest(input: {pullRequestId: $pr_id, commitHeadline: $commit_headline, commitBody: $commit_body, mergeMethod: MERGE}) {
    pullRequest {
      merged
      mergedAt
      state
      url
    }
  }
}
{"pr_id":"PR_kwDOABUDh85A8UqR",
"commit_headline":"Merge PR #16688: Windows CI: use coq-ci branch from Platform.",
"commit_body":"Reviewed-by: MSoegtropIMC\nCo-authored-by: MSoegtropIMC <MSoegtropIMC@users.noreply.github.com>\n"
}

view this post on Zulip Théo Zimmermann (Oct 19 2022 at 07:44):

Very likely this still doesn't work and this needs to be reported to GitHub. Someone will need to merge the PR with the merge script instead. (The problem appears to be specific to this PR since in the meantime another PR has been merged with coqbot.

view this post on Zulip Michael Soegtrop (Oct 19 2022 at 08:19):

One thing I noted: why am I mentioned as Co-Author? I am not aware that I contributed to the PR in any way (in a technical sense). I can't merge the traditional way before today evening when I am at home.

view this post on Zulip Théo Zimmermann (Oct 19 2022 at 08:25):

You are a co-author of the merge commit itself :smile:

view this post on Zulip Théo Zimmermann (Oct 19 2022 at 08:26):

We do this because coqbot doesn't impersonate users that request to merge a PR.

view this post on Zulip Théo Zimmermann (Oct 19 2022 at 14:30):

Pierre-Marie took care of merging with the merge script.

view this post on Zulip Théo Zimmermann (Oct 20 2022 at 17:49):

I got an answer from GitHub support. This was a permission error (coqbot-app not having the permission to update workflow files). This should have been a 403 instead of a 500 though.

view this post on Zulip Théo Zimmermann (Oct 20 2022 at 18:07):

Fixed by changing the permissions required by coqbot.


Last updated: Jan 31 2023 at 11:01 UTC