refactor(Channel/FixedPoint): inline single-use Kraus unitality conversion #6368
Workflow file for this run
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| 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 |