review.yml

name: PR Review

# 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: true

jobs:
  review:
    # 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') &&
      (
        github.event.comment.author_association == 'OWNER' ||
        github.event.comment.author_association == 'MEMBER' ||
        github.event.comment.author_association == 'COLLABORATOR'
      )
    runs-on: ubuntu-latest
    timeout-minutes: 120
    permissions:
      contents: read
      pull-requests: write
    steps:
      # Everything after `/review` is freeform focus text.
      - name: Extract instructions from /review comment
        id: get_args
        env:
          COMMENT_BODY: ${{ github.event.comment.body }}
        run: |
          EOF=$(openssl rand -hex 8)
          {
            echo "instructions<<$EOF"
            printf '%s\n' "$COMMENT_BODY" | sed -E '1s|^/review[[:space:]]*||'
            echo "$EOF"
          } >> "$GITHUB_OUTPUT"
        shell: bash

      # Prepend CompPoly-specific review precedent (naming/style conventions that
      # override the generic CONTRIBUTING.md rules) to the user's focus text, so
      # every review applies the project's real conventions and doesn't flag
      # sanctioned patterns. Comment body is read via env, never interpolated.
      - name: Build review instructions
        id: build_instructions
        env:
          USER_COMMENTS: ${{ steps.get_args.outputs.instructions }}
        run: |
          EOF=$(openssl rand -hex 8)
          {
            echo "final<<${EOF}"
            cat <<'PRECEDENT'
          Project precedent (CompPoly-specific conventions that override generic CONTRIBUTING.md rules — do NOT flag these as violations):

          Variable naming overrides (algebraic context):
            - Algebraic carrier types use R, M, G, F (rings, modules, groups, fields), not α, β.
            - Polynomial-typed values use p, q (e.g. CPolynomial, CMvPolynomial, CMlPolynomial), not just predicates.
            - Indices into vectors, lists, and Fin n use i, j, k regardless of underlying numeric type.
            - In algebraic lemma names that mirror Mathlib (e.g. pow_add, npow_add), exponent variables may be a, b.

          Style rules marked "preferred but not enforced" in CONTRIBUTING.md (the merged codebase uses both styles freely — do not flag):
            - "Use the where syntax for instances" — both `instance ... := ⟨...⟩` and `instance ... where` are accepted.
            - "Use manual dot notation for equality" — both `h.symm` and `Eq.symm h` are accepted.
            - "Use <| / |> to reduce nesting" — both pipe-style and parens are accepted.

          File scope of style rules:
            - The 100-character line-length rule applies ONLY to `.lean` source files. Do NOT flag long lines in `.md`, `.yml`, `.toml`, or any other non-Lean files. The enforced linter (`scripts/lint-style.py`) only processes `.lean` files.

          Review scope:
            - Flag ONLY lines introduced by this PR (the diff). Do not comment on pre-existing code that this PR did not modify.
          PRECEDENT
            if [ -n "${USER_COMMENTS}" ]; then
              printf '\n\nUser-supplied additional context:\n%s\n' "${USER_COMMENTS}"
            fi
            echo "${EOF}"
          } >> "$GITHUB_OUTPUT"
        shell: bash

      - uses: alexanderlhicks/lean4repo-utils/review@0.3
        with:
          github_token: ${{ secrets.GITHUB_TOKEN }}
          api_key: ${{ secrets.OPENROUTER_KEY }}
          pr_number: ${{ github.event.issue.number }}
          additional_comments: ${{ steps.build_instructions.outputs.final }}
          # Ground the review in this repo's curated knowledge base (spec/KB docs).
          spec_refs: 'docs/wiki'
          # 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).