Add GitHub Actions to build PDFs and comment on PRs

Use GitHub's recommended two-part approach [1][2] to separate building
the PDFs (which runs in the PR branch's context and has only a read-only
GH token) from commenting on the PR (which runs on the master branch and
has write access to the repository).

[1] https://securitylab.github.com/research/github-actions-preventing-pwn-requests/
[2] https://docs.github.com/en/actions/using-workflows/events-that-trigger-workflows#using-data-from-the-triggering-workflow

.github/actions/texlive/action.yaml

@@ -0,0 +1,15 @@
+name: texlive
+description: Run commands in a TeXLive docker image
+
+inputs:
+  run:
+    description: Commands to be executed
+    required: true
+
+runs:
+  using: docker
+  image: docker://texlive/texlive:latest
+  entrypoint: /bin/sh
+  args:
+    - -c
+    - ${{ inputs.run }}

.github/workflows/pr-comment.yaml

@@ -0,0 +1,74 @@
+name: Add PR comment
+
+on:
+  workflow_run:
+    workflows: ["Handle PDF pull request"]
+    types: [completed]
+
+jobs:
+  comment:
+    runs-on: ubuntu-latest
+    if: ${{ github.event.workflow_run.conclusion == 'success' }}
+    env:
+      GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }}
+      run_id: ${{ github.event.workflow_run.id }}
+
+    steps:
+      - uses: actions/checkout@v3
+
+      - name: Download artifacts
+        run: |
+          gh run download --dir artifact --name pdf $run_id
+          cat artifact/environ.txt >> $GITHUB_ENV
+
+      - name: Check out preview ref
+        run: |
+          git fetch --depth=1 origin refs/preview/$pr_number:pr || git fetch --depth=1 origin $base_sha:pr
+          git switch pr
+          rm -rf new diff
+          mv artifact/new artifact/diff .
+
+      - name: Compose comment
+        shell: python
+        env:
+          view_url: https://cdn.jsdelivr.net/gh/${{ github.repository }}@<SHA>
+        run: |
+          import os
+
+          head_sha = os.environ['head_sha']
+          view_url = os.environ['view_url']
+
+          files = []
+          links = []
+          for pdf in sorted(os.listdir("new")):
+              new_pdf = os.path.join("new", pdf)
+              diff_pdf = os.path.join("diff", pdf)
+
+              text = f"[{os.path.splitext(pdf)[0]}]({view_url}/{new_pdf})"
+              files.append(new_pdf)
+              if os.path.exists(diff_pdf):
+                  text += f" ([diff]({view_url}/{diff_pdf}))"
+                  files.append(diff_pdf)
+              links.append(text)
+
+          with open(os.environ['GITHUB_ENV'], 'a') as outf:
+              files_text = " ".join(files)
+              print(f"pdf_files={files_text}", file=outf)
+
+              links_text = ", ".join(links)
+              print(f"comment=Changed PDFs as of {head_sha}: {links_text}.", file=outf)
+
+      - name: Update preview ref
+        env:
+          GIT_AUTHOR_NAME: hts-specs bot
+          GIT_COMMITTER_NAME: hts-specs bot
+          EMAIL: [email protected]
+        run: |
+          git add -f $pdf_files
+          git commit --allow-empty -m "PDFs for PR #$pr_number as of $head_sha"
+          git push origin pr:refs/preview/$pr_number
+
+      - name: Add PR comment
+        shell: bash
+        run: |
+          gh pr comment --body "${comment//<SHA>/$(git rev-parse pr)}" $pr_number

.github/workflows/pr-pdfs-close.yaml

@@ -0,0 +1,19 @@
+name: Tidy up PDF pull request
+
+on:
+  pull_request_target:
+    paths: '*.tex'
+    types: [closed]
+
+jobs:
+  clean:
+    runs-on: ubuntu-latest
+    env:
+      GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }}
+      pr_number: ${{ github.event.number }}
+
+    steps:
+      - name: Remove preview ref
+        continue-on-error: true
+        run: |
+          gh api --method DELETE repos/$GITHUB_REPOSITORY/git/refs/preview/$pr_number

.github/workflows/pr-pdfs.yaml

@@ -0,0 +1,47 @@
+name: Handle PDF pull request
+
+on:
+  pull_request:
+    paths: '*.tex'
+
+jobs:
+  LaTeX:
+    runs-on: ubuntu-latest
+    steps:
+      - uses: actions/checkout@v3
+        with:
+          fetch-depth: 0
+
+      - name: Identify changed LaTeX documents
+        env:
+          pr_number: ${{ github.event.number }}
+          base_sha: ${{ github.event.pull_request.base.sha }}
+          head_sha: ${{ github.event.pull_request.head.sha }}
+        run: |
+          mergebase_sha=$(git merge-base $base_sha $head_sha)
+          echo "mergebase_sha=$mergebase_sha" >> $GITHUB_ENV
+          changed=$(git diff-tree --name-only --merge-base $base_sha $head_sha -- '*.tex' | tr '\n' ' ')
+          echo "changed=$changed" >> $GITHUB_ENV
+          echo "pdfs=$(ls -1 $changed | sed 's,^,new/,;s,tex$,pdf,' | tr '\n' ' ')" >> $GITHUB_ENV
+          echo "diffs=$(ls -1 $changed | sed 's,^,diff/,;s,tex$,pdf,' | tr '\n' ' ')" >> $GITHUB_ENV
+
+          echo "pr_number=$pr_number" > environ.txt
+          echo "base_sha=$base_sha" >> environ.txt
+          echo "head_sha=$head_sha" >> environ.txt
+          echo "mergebase_sha=$mergebase_sha" >> environ.txt
+
+      - name: Run LaTeX
+        uses: ./.github/actions/texlive
+        if:   ${{ env.changed }}
+        with:
+          run: make ${{ env.pdfs }} && make -k OLD=$mergebase_sha NEW=HEAD ${{ env.diffs }}
+
+      - uses: actions/upload-artifact@v3
+        with:
+          name: pdf
+          retention-days: 1
+          if-no-files-found: ignore
+          path: |
+            environ.txt
+            new/*.pdf
+            diff/*.pdf