ci(*): tweak synchronization bot behavior (#17693)

This changes the script to output a list of filenames and PR links, so that a quick scan on github can verify that the PR numbers are entered correctly in the yaml.

This also changes the user doing the committing to be the community user.

.github/workflows/add_port_comment.yml

@@ -13,43 +13,39 @@ jobs:
       - uses: actions/checkout@v3
 
       - name: install Python
-        uses: actions/setup-python@v1
+        uses: actions/setup-python@v3
         with:
           python-version: 3.8
 
       - name: install latest mathlibtools
         run: |
           pip install git+https://github.com/leanprover-community/mathlib-tools
 
-      - name: update docstrings
-        run: |
-          python ./scripts/add_port_comments.py
-          
       # multiline outputs are only supported in javascript
-      - name: generate message
+      - name: update docstrings and generate message
         uses: actions/github-script@v5
         id: generate-message
         with:
           script: |
-            prs = await exec.getExecOutput("bash",
-              ['-c', "git diff HEAD -U0 | grep -o -e 'https://github.com/leanprover-community/mathlib4/pull/[0-9]\\+' | sort -u"]);
-            pr_bullets = prs.stdout.trim().split('\n').map(x => "* " + x).join('\n'); 
-            console.log(pr_bullets);
-            core.setOutput("PR_LIST", pr_bullets); 
+            proc = await exec.getExecOutput("python", ["./scripts/add_port_comments.py"]);
+            console.log(proc.stdout);
+            core.setOutput("PR_LIST", proc.stdout); 
 
       - name: Create Pull Request
         uses: peter-evans/create-pull-request@v4
         with:
           base: master
-          commit-message: "chore(*): add mathlibport comments"
-          title: "chore(*): add mathlibport comments"
+          commit-message: "chore(*): add mathlib4 synchronization comments"
+          title: "chore(*): add mathlib4 synchronization comments"
+          author: leanprover-community-bot <leanprover.community@gmail.com>
           body: |
             Regenerated from the [port status wiki page](https://github.com/leanprover-community/mathlib/wiki/mathlib4-port-status).
             Relates to the following PRs:
             ${{ steps.generate-message.outputs.PR_LIST }}
 
             ---
             I am a bot; please check that I have not put a comment in a bad place before running `bors merge`!
+            If the PRs above don't match the file they are listed after, that means the port status page is wrong.
           labels: |
             easy
             awaiting-review

scripts/add_port_comments.py

@@ -70,6 +70,9 @@ def fname_for(import_path):
         fname = fname_for(iname)
         with open(fname) as f:
             fcontent = f.read()
-        fcontent = add_port_status(fcontent, f_status)
+        new_fcontent = add_port_status(fcontent, f_status)
+        if new_fcontent == fcontent:
+            continue
+        print(f'* `{iname}`: https://github.com/leanprover-community/mathlib4/pull/{f_status.mathlib4_pr}')
         with open(fname, 'w') as f:
-            f.write(fcontent)
+            f.write(new_fcontent)