claude-code-review.yml

name: Claude Code Review (Lean)

on:
  pull_request:
    types: [opened, synchronize, ready_for_review, reopened]
    paths:
      - "TNLean/**/*.lean"
      - "TNLean.lean"
      - "lakefile.toml"
      - "lean-toolchain"
      - "blueprint/src/**/*.tex"
      - "docs/paper-gaps/**/*.tex"
      - "docs/paper-gaps/**/*.bib"

concurrency:
  group: claude-review-${{ github.event.pull_request.number }}
  cancel-in-progress: false

jobs:
  claude-review:
    name: claude-review-${{ matrix.provider }}
    strategy:
      fail-fast: false
      matrix:
        provider: ${{ fromJson(vars.CLAUDE_CODE_REVIEW_PROVIDERS || format('["{0}"]', vars.CLAUDE_CODE_PROVIDER || 'anthropic')) }}
    # Repository variable kill switch:
    #   CLAUDE_REVIEW_ENABLED=false disables Claude-powered PR review.
    #   unset or any other value preserves the default enabled behavior.
    if: vars.CLAUDE_REVIEW_ENABLED != 'false'
    runs-on: ubuntu-latest
    permissions:
      contents: read
      pull-requests: write
      actions: read
      issues: write
      id-token: write

    env:
      CLAUDE_CODE_OAUTH_TOKEN: ${{ secrets.CLAUDE_CODE_OAUTH_TOKEN }}
      DEEPSEEK_API_KEY: ${{ secrets.DEEPSEEK_API_KEY }}
      ANTHROPIC_BASE_URL: ${{ vars.ANTHROPIC_BASE_URL }}
      CLAUDE_OPUS_MODEL: ${{ vars.CLAUDE_OPUS_MODEL }}
      CLAUDE_SONNET_MODEL: ${{ vars.CLAUDE_SONNET_MODEL }}
      DEEPSEEK_BASE_URL: https://api.deepseek.com/anthropic
      CLAUDE_ALLOWED_TOOLS: >
        Read,Glob,Grep,Bash(gh pr diff:*),Bash(gh pr view:*),Bash(gh pr comment:*),Bash(gh api graphql:*),Bash(lake build),Bash(lake exe cache get),Bash(lake update),Bash(lake env),Bash(lean *),Bash(elan *),Bash(grep *),mcp__github__*

    steps:
      - name: Check Claude review switch
        id: claude-switch
        env:
          CLAUDE_REVIEW_ENABLED: ${{ vars.CLAUDE_REVIEW_ENABLED }}
        run: |
          if [ "$CLAUDE_REVIEW_ENABLED" = "false" ]; then
            echo "skip=true" >> "$GITHUB_OUTPUT"
            echo "::notice::Skipping Claude code review: CLAUDE_REVIEW_ENABLED=false"
          else
            echo "skip=false" >> "$GITHUB_OUTPUT"
          fi

      - name: Check if head commit is a bot auto-fix
        if: steps.claude-switch.outputs.skip != 'true'
        id: bot-check
        uses: actions/github-script@v8
        with:
          script: |
            // Skip review for auto-fix bot commits to avoid the
            // review → auto-fix → review ping-pong cascade.
            // The auto-fix workflow will re-trigger review after its
            // fixes, but we only want to review human-authored pushes
            // and the final bot-fix result (detected by iteration cap).
            const { data: commit } = await github.rest.repos.getCommit({
              owner: context.repo.owner,
              repo: context.repo.repo,
              ref: context.payload.pull_request.head.sha
            });
            const msg = commit.commit.message;
            const isBot = /^\[(claude|codex)-(auto|review)-fix\]/.test(msg);
            core.setOutput('skip', isBot ? 'true' : 'false');
            if (isBot) core.notice(`Skipping review for bot-fix commit: ${msg.split('\n')[0]}`);

      - name: Check review provider token
        if: steps.claude-switch.outputs.skip != 'true' && steps.bot-check.outputs.skip != 'true'
        id: provider-token
        env:
          REVIEW_PROVIDER: ${{ matrix.provider }}
          CLAUDE_CODE_OAUTH_TOKEN: ${{ secrets.CLAUDE_CODE_OAUTH_TOKEN }}
          DEEPSEEK_API_KEY: ${{ secrets.DEEPSEEK_API_KEY }}
        run: |
          set -euo pipefail
          case "$REVIEW_PROVIDER" in
            anthropic) provider_token="$CLAUDE_CODE_OAUTH_TOKEN" ;;
            deepseek) provider_token="$DEEPSEEK_API_KEY" ;;
            *)
              echo "::error::Unsupported review provider: $REVIEW_PROVIDER"
              exit 1
              ;;
          esac
          if [ -n "$provider_token" ]; then
            echo "skip=false" >> "$GITHUB_OUTPUT"
          else
            echo "skip=true" >> "$GITHUB_OUTPUT"
            echo "reason=$REVIEW_PROVIDER token is not configured" >> "$GITHUB_OUTPUT"
          fi

      - name: Checkout repository under review
        if: steps.claude-switch.outputs.skip != 'true' && steps.bot-check.outputs.skip != 'true' && steps.provider-token.outputs.skip != 'true'
        uses: actions/checkout@v6
        with:
          fetch-depth: 1

      - name: Checkout trusted automation
        if: steps.claude-switch.outputs.skip != 'true' && steps.bot-check.outputs.skip != 'true' && steps.provider-token.outputs.skip != 'true'
        uses: actions/checkout@v6
        with:
          ref: ${{ github.event.pull_request.base.ref }}
          path: .trusted-actions
          fetch-depth: 1

      - name: Set up Lean toolchain and cache
        if: steps.claude-switch.outputs.skip != 'true' && steps.bot-check.outputs.skip != 'true' && steps.provider-token.outputs.skip != 'true'
        uses: texra-ai/lean-env-action@v1
        with:
          use-github-cache: false

      - name: Run Claude Code Review
        if: steps.claude-switch.outputs.skip != 'true' && steps.bot-check.outputs.skip != 'true' && steps.provider-token.outputs.skip != 'true'
        id: claude-review
        uses: LionSR/agent-ci-actions@v1
        with:
          provider: ${{ matrix.provider }}
          model-tier: opus
          allowed-bots: 'claude,chatgpt-codex-connector,cursor[bot],cursor,copilot-pull-request-reviewer'
          plugin_marketplaces: |
            https://github.com/anthropics/claude-code.git
            https://github.com/leanprover/skills.git
          plugins: |
            code-review@claude-code-plugins
            lean@leanprover
          claude-prompt-file: .trusted-actions/.github/prompts/claude-code-review-prompt.md
          claude-prompt-context: |
            PR number: ${{ github.event.pull_request.number }}
            Repository: ${{ github.repository }}
            Repository owner: ${{ github.repository_owner }}
            Repository name: ${{ github.event.repository.name }}
            Review this Lean 4 pull request: ${{ github.repository }}/pull/${{ github.event.pull_request.number }}
            Review provider: ${{ matrix.provider }}
            Trigger event: ${{ github.event.action }}
          system-prompt-file: .trusted-actions/.github/prompts/claude-code-review-system-prompt.md