feat: add /check-golf bot verifying statements are unchanged

.github/workflows/check-golf.yml

@@ -0,0 +1,72 @@
+# Reacts to a `/check-golf` comment on a pull request. It verifies that the PR
+# only golfs proofs -- i.e. that no declaration *statement* (signature/type)
+# changed, only proofs and bodies -- and posts the findings as a single PR
+# comment, editing that comment in place on subsequent runs.
+#
+# The check runs on `issue_comment`, so it uses the workflow file from the
+# default branch and only parses the PR's Lean sources textually (it does not
+# build them).
+
+name: Check golf
+
+on:
+  issue_comment:
+    types: [created]
+
+# Only the permissions needed to read the repo and upsert a PR comment.
+permissions:
+  contents: read
+  pull-requests: write
+
+jobs:
+  check-golf:
+    name: Verify only proofs changed
+    # Run only for `/check-golf` comments posted on a pull request.
+    if: >-
+      github.event.issue.pull_request &&
+      contains(github.event.comment.body, '/check-golf')
+    runs-on: ubuntu-latest
+    steps:
+      - name: Acknowledge the command
+        env:
+          GH_TOKEN: ${{ secrets.GITHUB_TOKEN }}
+          COMMENT_ID: ${{ github.event.comment.id }}
+        run: |
+          gh api --method POST \
+            "repos/${{ github.repository }}/issues/comments/${COMMENT_ID}/reactions" \
+            -f content=eyes || true
+
+      - name: Checkout repository
+        uses: actions/checkout@v4
+        with:
+          fetch-depth: 0
+
+      - name: Resolve base and head revisions
+        id: refs
+        env:
+          GH_TOKEN: ${{ secrets.GITHUB_TOKEN }}
+          PR: ${{ github.event.issue.number }}
+        run: |
+          base_branch=$(gh pr view "$PR" --json baseRefName -q .baseRefName)
+          head_sha=$(gh pr view "$PR" --json headRefOid -q .headRefOid)
+          git fetch --no-tags origin "$base_branch"
+          git fetch --no-tags origin "pull/$PR/head:check-golf-head"
+          merge_base=$(git merge-base "origin/$base_branch" "$head_sha")
+          echo "base=$merge_base" >> "$GITHUB_OUTPUT"
+          echo "head=$head_sha" >> "$GITHUB_OUTPUT"
+
+      - name: Set up Python
+        uses: actions/setup-python@v5
+        with:
+          python-version: '3.12'
+
+      - name: Run check-golf and upsert the report comment
+        env:
+          GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }}
+        run: |
+          python scripts/check_golf.py \
+            --base "${{ steps.refs.outputs.base }}" \
+            --head "${{ steps.refs.outputs.head }}" \
+            --repo "${{ github.repository }}" \
+            --pr "${{ github.event.issue.number }}" \
+            --post

scripts/README.md

@@ -34,3 +34,20 @@ This linter may need running a number of times.
 - `lake exe module_doc_lint` : Checks that module documentation is laid out according to a set standard. This does not check any file in the list `./scripts/MetaPrograms/module_doc_no_lint.txt`. Slowly we will empty this list of files.
 - `lake exe spelling` : Checks the spelling of words in Physlib against a given list
   of correctly spelled words which can be found in `./scripts/MetaPrograms/spellingWords.txt`
+
+## Checking golf pull requests
+
+- `scripts/check_golf.py` : Verifies that a pull request only *golfs* proofs, i.e.
+  that no declaration statement (its signature/type) changed and only proofs and
+  definition bodies changed. Comment `/check-golf` on a PR to run it via the
+  [`check-golf`](../.github/workflows/check-golf.yml) workflow; the bot posts its
+  findings as a single PR comment and edits that same comment on subsequent runs.
+  To run it locally against two revisions:
+
+  ```
+  scripts/check_golf.py --base <merge-base> --head <head-sha>
+  ```
+
+  It parses the changed Lean files textually (no build required): comments and
+  whitespace are ignored, and `by` proof terms embedded inside a type are treated
+  as proofs (proof-irrelevant). Anonymous instances and `example`s are not tracked.