ci: deploy lean4repo-utils@0.3 review+summary from the README example

alexanderlhicks · claude · alexanderlhicks · commit 3da5d25dca77 · 2026-07-24T05:26:34.000+01:00
Regenerate both AI PR workflows as fresh copies of the canonical example
workflows in the action READMEs, pinned @0.3, using default models:
- review: ChatOps-only (/review from a repo member), review@0.3, OPENROUTER_KEY.
- summary: every-PR pull_request_target, summary@0.3, OPENROUTER_KEY, default model.

Supersedes the earlier per-repo migration so this repo runs the identical,
current, example-based workflow as the rest of the fleet.

NOTE: this replaces the bespoke review workflow that auto-resolved KB paper
citations (docs/kb/_generated/lean-citations.json) into spec_refs. That
auto-grounding is intentionally dropped for the clean example baseline; re-add
it on top of this if wanted (the consolidated action still accepts spec_refs and
auto-extracts refs from the /review comment text).

Co-Authored-By: Claude Opus 4.8 (1M context) &lt;noreply@anthropic.com&gt;
diff --git a/.github/workflows/review.yml b/.github/workflows/review.yml
@@ -1,30 +1,23 @@
 name: PR Review
 
-# Trusted CHATOPS-ONLY deployment of the consolidated OpenRouter review action
-# (lean4repo-utils/review@main). Invoked by a maintainer commenting `/review` on a PR.
-# The auto pull_request trigger is intentionally dropped for now.
+# Review runs ONLY on demand, via a `/review` comment from a repo member. It is
+# deliberately NOT run on PR open: the review path builds and elaborates the
+# PR's Lean code with the OpenRouter secret and a write token in scope, so until
+# the two-stage secret-free split (S2) lands, running it is safe only for code a
+# trusted maintainer has chosen to review. See the review action README.
 on:
   issue_comment:
     types: [created]
 
 concurrency:
   group: ${{ github.workflow }}-${{ github.event.issue.number }}
-  cancel-in-progress: false
-
-# Least privilege: the reviewer's lean_tools execute model-directed Lean IO and the
-# action builds the PR-head code, so a token exfiltrated there must not be able to push
-# or merge. Only what posting a review needs.
-permissions:
-  contents: read
-  pull-requests: write
-  issues: write
+  cancel-in-progress: true
 
 jobs:
   review:
-    # Chatops only, gated to trusted members. NOTE: `/review` here is a coarse prefix
-    # match — a member typing `/reviewer` would also match; harmless under the member
-    # gate, tighten to a word boundary if this ever opens to untrusted commenters.
+    # The COMMENT author (not the PR author) is the trust boundary.
     if: >-
+      github.event_name == 'issue_comment' &&
       github.event.issue.pull_request &&
       startsWith(github.event.comment.body, '/review') &&
       (
@@ -33,99 +26,35 @@ jobs:
         github.event.comment.author_association == 'COLLABORATOR'
       )
     runs-on: ubuntu-latest
-    timeout-minutes: 240
+    timeout-minutes: 120
+    permissions:
+      contents: read
+      pull-requests: write
     steps:
-      # Parse the /review comment: `Internal:` lines → manual spec/KB refs, everything
-      # under `External:`/`Comments:` → free-text instructions (the action auto-extracts
-      # any URLs it mentions). Comment body is passed via env, never interpolated into
-      # the run: body (GHA expression-injection guard).
-      - name: Extract arguments from comment
+      # Everything after `/review` is freeform focus text; URLs and existing
+      # repo paths it mentions become review context automatically.
+      - name: Extract instructions from /review comment
         id: get_args
         env:
           COMMENT_BODY: ${{ github.event.comment.body }}
-        shell: bash
         run: |
           EOF=$(openssl rand -hex 8)
-          awk -v eof="$EOF" -v gh_out="$GITHUB_OUTPUT" '
-            BEGIN { spec=""; com=""; section="" }
-            /^External:/ { section="com"; next }
-            /^Internal:/ { section="spec"; next }
-            /^Comments:/ { section="com"; next }
-            {
-              gsub(/\r/, "", $0); gsub(/^[ \t]+|[ \t]+$/, "", $0);
-              if ($0 == "" || $0 == "/review") { next }
-              if (section == "spec") { sub(/^- +/, ""); spec = (spec=="" ? $0 : spec "," $0) }
-              else if (section == "com") { com = (com=="" ? $0 : com "\n" $0) }
-            }
-            END {
-              printf "manual_spec_refs=%s\n", spec >> gh_out
-              printf "additional_comments<<%s\n%s\n%s\n", eof, com, eof >> gh_out
-            }
-          ' <<< "$COMMENT_BODY"
-
-      # Unguided KB grounding: map the PR''s changed .lean files to the papers they cite
-      # (docs/kb/_generated/lean-citations.json) and pass those KB pages as spec_refs, so
-      # a plain /review is grounded in the right paper summaries with no manual guidance.
-      # Read the citation JOIN from the BASE ref (data-only, fork-safe); do NOT execute
-      # any checked-out repo script. (The KB page CONTENT is read by the action from the
-      # PR head — acceptable for this trusted, manually-inspected pilot; base-ref content
-      # reading is part of the S2/S7 hardening.)
-      - name: Resolve KB context (base-ref citation join)
-        id: kb
-        env:
-          GH_TOKEN: ${{ secrets.GITHUB_TOKEN }}
-          PR_NUMBER: ${{ github.event.issue.number }}
-          MANUAL_SPEC_REFS: ${{ steps.get_args.outputs.manual_spec_refs }}
+          {
+            echo "instructions<<$EOF"
+            printf '%s\n' "$COMMENT_BODY" | sed -E '1s|^/review[[:space:]]*||'
+            echo "$EOF"
+          } >> "$GITHUB_OUTPUT"
         shell: bash
-        run: |
-          set -euo pipefail
-          BASE_SHA="$(gh api "repos/$GITHUB_REPOSITORY/pulls/$PR_NUMBER" --jq '.base.sha')"
-          gh api "repos/$GITHUB_REPOSITORY/pulls/$PR_NUMBER/files" --paginate --jq '.[].filename' > /tmp/changed.txt
-          if gh api "repos/$GITHUB_REPOSITORY/contents/docs/kb/_generated/lean-citations.json?ref=$BASE_SHA" \
-               --jq '.content' 2>/dev/null | base64 -d > /tmp/citations.json; then :; else
-            echo "No lean-citations.json on base ref; proceeding without KB spec_refs."
-            echo '{}' > /tmp/citations.json
-          fi
-          # Join is pure data: filenames + JSON read from files, never interpolated.
-          spec_refs="$(python3 - <<'PY'
-          import json, os
-          try:
-              cites = json.load(open('/tmp/citations.json')).get('files', {})
-          except Exception:
-              cites = {}
-          changed = [l.strip() for l in open('/tmp/changed.txt') if l.strip().endswith('.lean')]
-          keys = []
-          for f in changed:
-              for k in cites.get(f, []):
-                  if k not in keys:
-                      keys.append(k)
-          refs = [f"docs/kb/papers/{k}.md" for k in keys]
-          # Merge any manual `Internal:` refs from the /review comment (dedup, keep order).
-          for r in (os.environ.get("MANUAL_SPEC_REFS", "") or "").split(","):
-              r = r.strip()
-              if r and r not in refs:
-                  refs.append(r)
-          print(",".join(refs))
-          PY
-          )"
-          echo "spec_refs=$spec_refs" >> "$GITHUB_OUTPUT"
-          echo "Resolved KB spec_refs: ${spec_refs:-(none)}"
 
-      - name: AI review
-        uses: alexanderlhicks/lean4repo-utils/review@main
+      - uses: alexanderlhicks/lean4repo-utils/review@0.3
         with:
           github_token: ${{ secrets.GITHUB_TOKEN }}
           api_key: ${{ secrets.OPENROUTER_KEY }}
           pr_number: ${{ github.event.issue.number }}
-          # Auto-pulled KB paper pages for the changed files + any manual Internal: refs.
-          spec_refs: ${{ steps.kb.outputs.spec_refs }}
-          additional_comments: ${{ steps.get_args.outputs.additional_comments }}
-          # Coverage-first budget control: this sizes/trims prompts for large PRs,
-          # but advisory mode does not stop later files from being reviewed.
-          # Source these from workflow config, never PR content.
-          # llm_max_run_tokens: "400000"
-          # llm_budget_mode: advisory
-          # model: omitted → the action's default OpenRouter slug. Set an explicit slug
-          # here if you want a specific model for the pilot.
-          # lean_tools defaults true (full-quality, compiler-grounded review — trusted
-          # pilot). enable_web_search defaults false (web-search fees are not token-bounded).
+          # URLs and repo paths mentioned in the /review comment are extracted
+          # into external/spec/repo context automatically.
+          additional_comments: "${{ steps.get_args.outputs.instructions }}"
+          # Everything else uses the action defaults (deep agents on z-ai/glm-5.2,
+          # verification on deepseek/deepseek-v4-pro, lean_tools + verify_findings
+          # on). See the review action README to override models or tune
+          # spec_refs / escape_hatch_allowlist / dependent_impact_max.
diff --git a/.github/workflows/summary.yml b/.github/workflows/summary.yml
@@ -1,5 +1,10 @@
 name: 'PR Summary'
 
+# Summary runs on every PR update (open + each new commit). It is SAFE under
+# pull_request_target — where the OpenRouter secret and a write token are in
+# scope even for fork PRs — because it never builds or executes PR code: it
+# reads the diff and committed source as data, and reads its policy file from
+# the BASE ref (S4). See the summary action README.
 on:
   pull_request_target:
     types: [opened, synchronize, reopened]
@@ -9,25 +14,23 @@ concurrency:
   cancel-in-progress: true
 
 permissions:
-  contents: read        # required: the action checks out the PR head to read the diff
-  pull-requests: write  # required: post/update the summary comment
-  issues: read          # optional: link affected sorries to `proof wanted` issues
+  contents: read
+  pull-requests: write
+  issues: read
 
 jobs:
   summarize:
     runs-on: ubuntu-latest
-    timeout-minutes: 20
     steps:
       - name: Generate PR Summary
-        uses: alexanderlhicks/lean-summary-workflow@main
+        uses: alexanderlhicks/lean4repo-utils/summary@0.3
         with:
           github_token: ${{ secrets.GITHUB_TOKEN }}
           api_key: ${{ secrets.OPENROUTER_KEY }}
-          # model: inherits the action default (deepseek/deepseek-v4-flash).
-          #        Set `model: <openrouter-slug>` here to override for this repo only.
           github_repository: ${{ github.repository }}
           pr_number: ${{ github.event.pull_request.number }}
-          additional_instructions_path: 'CONTRIBUTING.md'
-          validate_title: 'true'
-          upstream_path: 'ArkLib/ToMathlib/'
-          # Other optional knobs (reasoning_effort, max_*_diff_chars): see the action README.
+          # Uses the default model (deepseek/deepseek-v4-flash). Optional knobs:
+          # model: <any OpenRouter slug>       # e.g. google/gemini-3-flash-preview
+          # additional_instructions_path: 'CONTRIBUTING.md'  # default; read from the base ref
+          # validate_title: 'true'             # enforce conventional-commit PR titles
+          # upstream_path: 'ToMathlib/'        # remind on changes under this prefix
