@@ -42,6 +42,7 @@ pipeline {
     string(name: 'pull_request_baseline', defaultValue: 'master', description: 'The branch a pull request is compared against. Its newest run has to come from pull_request_node, or the report compares the machines as much as the pull request.')
     string(name: 'pull_request_config', defaultValue: 'configs/conf.json', description: 'What a pull request run tests. A full run takes days, so a smaller configuration file is often the better question to ask.')
     choice(name: 'pull_request_node', choices: ['ryzen-5950x-1', 'ryzen-5950x-2-1', 'ryzen-9950x'], description: 'The machine a pull request runs on. The default is the one that produces the master runs it is compared against.')
+    booleanParam(name: 'pull_request_comment', defaultValue: false, description: 'Post the summary of a pull request run as a comment on the pull request, replacing the one an earlier run posted. Needs a github-token credential; without it the report is still written and published, only not commented.')
     booleanParam(name: 'drop_stale_pull_request_tables', defaultValue: false, description: 'Drop the pr-<N> tables of pull requests that have been merged or closed, and of those tested more than 60 days ago. The reports published for them are not touched.')
   }
   environment {
@@ -634,9 +635,19 @@ pipeline {
           }
         }
         sh 'rm -rf history'
-        sh "./pr-report.py '${pullRequest()}' --baseline='${(params.pull_request_baseline ?: 'master').trim()}'"
-        // The summary to comment on the pull request with, in the build log
-        // until there is a token to post it with.
+        script {
+          def report = "./pr-report.py '${pullRequest()}' --baseline='${(params.pull_request_baseline ?: 'master').trim()}'"
+          if (params.pull_request_comment) {
+            // Whoever the token belongs to is who the comment comes from.
+            withCredentials([string(credentialsId: 'github-token', variable: 'GITHUB_TOKEN')]) {
+              sh "${report} --comment"
+            }
+          } else {
+            sh report
+          }
+        }
+        // The summary is in the build log as well, so a run without a token
+        // still leaves it somewhere to copy from.
         sh 'cat history/pr-*/00_comment.md'
         sshPublisher(publishers: [sshPublisherDesc(configName: 'LibraryTestingReports', transfers: [sshTransfer(sourceFiles: 'history/**')])])
       }
 
@@ -288,6 +288,14 @@ kind of page as the nightly regression reports, next to `00_comment.md`, a
 summary to comment on the pull request with. Both are published with the other
 reports.
 
+`--comment` posts that summary on the pull request, and replaces it rather than
+adding to it when the same pull request is tested again. It posts as whoever the
+token belongs to: `GITHUB_TOKEN` or `GH_TOKEN` in the environment, or the account
+[`gh`](https://cli.github.com) is logged in as. In Jenkins it is the
+`pull_request_comment` parameter, which takes the token from a `github-token`
+credential; without one the report is still written and published, and the
+summary is in the build log.
+
 Two things make a difference mean something other than "the pull request did
 this", and the report says so when they apply: **the machine**, since two runs
 produced on different hardware compare the hardware as much as the change, and
 
@@ -10,7 +10,8 @@
 what each phase cost - only the two runs it is given come from two branches.
 """
 
-import argparse, codecs, datetime, html, os, re, time
+import argparse, codecs, datetime, html, json, os, re, subprocess, time
+import urllib.error, urllib.request
 import shared, resultsdb
 from omcommon import friendlyStr, multiple_replace
 
@@ -24,6 +25,7 @@
 parser.add_argument('--historypath', default="history")
 parser.add_argument('--githuburl', default="https://github.com/OpenModelica/OpenModelica")
 parser.add_argument('--markdown', default="", help='where to write the summary to comment on the pull request with (default: <historypath>/<branch>/00_comment.md)')
+parser.add_argument('--comment', action='store_true', help='post that summary on the pull request, replacing the one posted by an earlier run')
 resultsdb.addArgument(parser)
 args = parser.parse_args()
 
@@ -45,6 +47,7 @@
 branch = "pr-%s" % pr
 baseline = args.baseline.split("/")[-1]
 prurl = "%s/pull/%s" % (args.githuburl, pr)
+repo = args.githuburl.split("github.com/")[-1].strip("/")
 
 db = resultsdb.connect(args.db)
 cursor = db.cursor()
@@ -213,6 +216,54 @@ def classify(group, times):
   return (colour, " ".join(msgs),
           "performance improved" if colour == "betterPerformance" else "performance regression")
 
+# A run of the same pull request replaces the comment of the one before it
+# rather than adding to a pile; this is how it recognises its own.
+COMMENTMARKER = "<!-- openmodelica-library-testing: pull request report -->"
+
+def githubToken():
+  """A token to post with: the environment, or whoever gh is logged in as."""
+  for var in ["GITHUB_TOKEN", "GH_TOKEN"]:
+    if os.environ.get(var):
+      return os.environ[var]
+  try:
+    return subprocess.check_output(["gh", "auth", "token"],
+                                   stderr=subprocess.DEVNULL).decode("utf-8").strip()
+  except Exception:
+    return None
+
+def github(url, token, data=None, method=None):
+  request = urllib.request.Request(
+      url, method=method,
+      data=json.dumps(data).encode("utf-8") if data is not None else None,
+      headers={"Accept": "application/vnd.github+json",
+               "Authorization": "Bearer %s" % token,
+               "Content-Type": "application/json"})
+  return json.loads(urllib.request.urlopen(request).read().decode("utf-8"))
+
+def postComment(number, body):
+  """Post the summary on the pull request, or update the one already there."""
+  token = githubToken()
+  if not token:
+    return ("No token to comment with: set GITHUB_TOKEN, or log in with gh. "
+            "The comment is in %s." % markdownname)
+  api = "https://api.github.com/repos/%s/issues" % repo
+  try:
+    page = 1
+    while True:
+      comments = github("%s/%s/comments?per_page=100&page=%d" % (api, number, page), token)
+      for comment in comments:
+        if COMMENTMARKER in (comment.get("body") or ""):
+          github(comment["url"], token, {"body": body}, method="PATCH")
+          return "Updated %s" % comment["html_url"]
+      if len(comments) < 100:
+        break
+      page += 1
+    return "Commented on %s" % github("%s/%s/comments" % (api, number), token,
+                                      {"body": body})["html_url"]
+  except urllib.error.HTTPError as e:
+    raise SystemExit("Could not comment on %s#%s: %s\n%s"
+                     % (repo, number, e, e.read().decode("utf-8", "replace")))
+
 counts = {"improved": 0, "regression": 0, "performance improved": 0, "performance regression": 0}
 rows = []
 markdownrows = []
@@ -337,8 +388,12 @@ def classify(group, times):
 markdown += ["- %s" % c.replace("&rarr;", "->") for c in caveats + [note]]
 markdown += ["", "</details>", "", "---", "Generated by the OpenModelica library testing"]
 markdownname = args.markdown or os.path.join(historydir, "00_comment.md")
+comment = "\n".join([COMMENTMARKER] + markdown) + "\n"
 with codecs.open(markdownname, "w", encoding="utf-8") as fout:
-  fout.write("\n".join(markdown) + "\n")
+  fout.write(comment)
+
+if args.comment:
+  print(postComment(pr, comment))
 
 print("%s: %s" % (branch, summary))
 print("Report:  %s" % os.path.join(historydir, reportname))