refactor(PEPS): use pi congruence for torus boundary casts #37945
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 (Lean) | |
| on: | |
| issue_comment: | |
| types: [created] | |
| pull_request_review_comment: | |
| types: [created] | |
| issues: | |
| types: [opened, assigned] | |
| pull_request_review: | |
| types: [submitted] | |
| concurrency: | |
| group: bot-respond-${{ github.event.issue.number || github.event.pull_request.number || github.event.comment.id }} | |
| cancel-in-progress: false | |
| env: | |
| GH_TOKEN: ${{ secrets.BOT_PAT || secrets.GITHUB_TOKEN }} | |
| jobs: | |
| claude: | |
| # Skip when: | |
| # - sender is a bot (e.g. Copilot reposting a review that contains "@claude") | |
| # — claude-code-action rejects non-collaborator actors anyway. | |
| # - the triggering author lacks write access (author_association not in | |
| # OWNER/MEMBER/COLLABORATOR). Defense-in-depth: this workflow runs with | |
| # write permissions and repo secrets, so prompt-injection from untrusted | |
| # commenters must not start the runner. | |
| if: | | |
| github.event.sender.type != 'Bot' && ( | |
| (github.event_name == 'issue_comment' && contains(github.event.comment.body, '@claude') && contains(fromJSON('["OWNER","MEMBER","COLLABORATOR"]'), github.event.comment.author_association)) || | |
| (github.event_name == 'pull_request_review_comment' && contains(github.event.comment.body, '@claude') && contains(fromJSON('["OWNER","MEMBER","COLLABORATOR"]'), github.event.comment.author_association)) || | |
| (github.event_name == 'pull_request_review' && contains(github.event.review.body, '@claude') && contains(fromJSON('["OWNER","MEMBER","COLLABORATOR"]'), github.event.review.author_association)) || | |
| (github.event_name == 'issues' && (contains(github.event.issue.body, '@claude') || contains(github.event.issue.title, '@claude')) && contains(fromJSON('["OWNER","MEMBER","COLLABORATOR"]'), github.event.issue.author_association)) | |
| ) | |
| runs-on: ubuntu-latest | |
| timeout-minutes: 45 | |
| env: | |
| CLAUDE_CODE_PROVIDER: ${{ vars.CLAUDE_CODE_PROVIDER || 'anthropic' }} | |
| 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 }} | |
| permissions: | |
| contents: write | |
| pull-requests: write | |
| issues: write | |
| id-token: write | |
| actions: read # Required for Claude to read CI results on PRs | |
| steps: | |
| - name: Checkout repository | |
| uses: actions/checkout@v6 | |
| with: | |
| fetch-depth: 1 | |
| token: ${{ env.GH_TOKEN }} | |
| - name: Set up Lean toolchain and cache | |
| uses: texra-ai/lean-env-action@v1 | |
| - name: Install blueprint TeX stack | |
| uses: texra-ai/lean-env-action/blueprint-system-deps@v1 | |
| - name: Install leanblueprint | |
| uses: texra-ai/lean-env-action/leanblueprint@v1 | |
| - name: Run Claude Code | |
| id: claude | |
| uses: LionSR/agent-ci-actions@v1 | |
| with: | |
| provider: ${{ env.CLAUDE_CODE_PROVIDER }} | |
| model-tier: opus | |
| allowed-bots: 'claude,chatgpt-codex-connector,cursor[bot],cursor,copilot-pull-request-reviewer' | |
| branch-name-template: "{{prefix}}{{entityType}}-{{entityNumber}}-{{description}}" | |
| allowed_tools_preset: claude-interactive | |
| allowed_tools_preset_map_file: .github/allowed-tools.json | |
| # This is an optional setting that allows Claude to read CI results on PRs | |
| additional-permissions: | | |
| actions: read | |
| # Load Lean skills from the official leanprover skills repository | |
| plugin_marketplaces: 'https://github.com/leanprover/skills.git' | |
| plugins: 'lean@leanprover' | |
| system-prompt-file: .github/prompts/claude-code-system-prompt.md | |
| - name: Auto-create PR for completed issue work | |
| if: | | |
| !cancelled() && | |
| steps.claude.outcome == 'success' && | |
| (github.event_name == 'issues' || | |
| (github.event_name == 'issue_comment' && !github.event.issue.pull_request)) | |
| uses: LionSR/agent-ci-actions/auto-create-issue-pr@v1 | |
| with: | |
| issue-number: ${{ github.event.issue.number }} | |
| repo: ${{ github.repository }} | |
| branch-prefix: 'claude/issue-' | |
| creator-name: 'Claude Code action' | |
| autofix-label: 'auto-fix-claude' | |
| event-name: ${{ github.event_name }} | |
| comment-body: ${{ github.event.comment.body || '' }} | |
| issue-body: ${{ github.event.issue.body || '' }} | |
| issue-title: ${{ github.event.issue.title || '' }} | |
| gh-token: ${{ env.GH_TOKEN }} |