coqbot merge now issue · coqbot devs & users

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"}}

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
    }
  }
}

{"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"}

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.

Michael Soegtrop (Oct 19 2022 at 07:34):

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

Théo Zimmermann (Oct 19 2022 at 07:40):

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"
}

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.

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.

Théo Zimmermann (Oct 19 2022 at 08:25):

Théo Zimmermann (Oct 19 2022 at 08:26):

Théo Zimmermann (Oct 19 2022 at 14:30):

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.

Stream: coqbot devs & users

Topic: coqbot merge now issue

Théo Zimmermann (Oct 18 2022 at 16:12):