Bump the production group across 1 directory with 18 updates #6
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: Lean4 specs | ||
| on: | ||
| pull_request: | ||
| paths: | ||
| - "specs/**" | ||
| - "lakefile.lean" | ||
| - "lean-toolchain" | ||
| - "src/lean4-generator.ts" | ||
| - ".github/workflows/lean4-ci.yml" | ||
| push: | ||
| branches: [main, master] | ||
| paths: | ||
| - "specs/**" | ||
| - "lakefile.lean" | ||
| - "lean-toolchain" | ||
| - "src/lean4-generator.ts" | ||
| jobs: | ||
| lean4-specs: | ||
| runs-on: ubuntu-latest | ||
| permissions: | ||
| contents: read | ||
| pull-requests: write | ||
| steps: | ||
| - name: Checkout | ||
| uses: actions/checkout@v4 | ||
| - name: Build specs (lake via lean-action) | ||
| uses: leanprover/lean-action@v1 | ||
| with: | ||
| auto-config: "true" | ||
| test: "false" | ||
| - name: Report sorry count | ||
| env: | ||
| # Fail the job only when SPECSYNC_PROOF_GATE=strict (repo variable or secret). | ||
| SPECSYNC_PROOF_GATE: ${{ vars.SPECSYNC_PROOF_GATE || 'soft' }} | ||
| run: | | ||
| set -euo pipefail | ||
| if [ ! -d specs ]; then | ||
| echo "No specs/ directory — nothing to report" | ||
| exit 0 | ||
| fi | ||
| # Count sorry tokens outside comments (block /- -/ and line --). | ||
| # Note: avoid embedding nested /- -/ examples inside docs (breaks strip). | ||
| TOTAL=$(python3 - <<'PY' | ||
| import re, pathlib | ||
| text = "" | ||
| for p in pathlib.Path("specs").rglob("*.lean"): | ||
| text += p.read_text(encoding="utf-8", errors="ignore") + "\n" | ||
| # Remove block comments iteratively so nested markers in docs do not leak tokens. | ||
| prev = None | ||
| while prev != text: | ||
| prev = text | ||
| text = re.sub(r"/-.*?-/", " ", text, count=1, flags=re.S) | ||
| stripped = re.sub(r"--[^\n]*", " ", text) | ||
| print(len(re.findall(r"(?:^|[^A-Za-z0-9_])sorry(?=[^A-Za-z0-9_]|$)", stripped))) | ||
| PY | ||
| ) | ||
| TOTAL=${TOTAL:-0} | ||
| echo "SpecSync Lean sorry count: ${TOTAL}" | ||
| echo "sorry_count=${TOTAL}" >> "$GITHUB_STEP_SUMMARY" | ||
| echo "### SpecSync Lean \`sorry\` report" >> "$GITHUB_STEP_SUMMARY" | ||
| echo "" >> "$GITHUB_STEP_SUMMARY" | ||
| echo "Found **${TOTAL}** \`sorry\` occurrence(s) under \`specs/\`." >> "$GITHUB_STEP_SUMMARY" | ||
| echo "Gate: \`SPECSYNC_PROOF_GATE=${SPECSYNC_PROOF_GATE}\` (fail only when \`strict\`)." >> "$GITHUB_STEP_SUMMARY" | ||
| if [ "$SPECSYNC_PROOF_GATE" = "strict" ] && [ "$TOTAL" -gt 0 ]; then | ||
| echo "SPECSYNC_PROOF_GATE=strict and sorry found — failing" | ||
| exit 1 | ||
| fi | ||
| - name: Comment on PR with build summary | ||
| if: github.event_name == 'pull_request' && success() | ||
| uses: actions/github-script@v7 | ||
| with: | ||
| script: | | ||
| const body = [ | ||
| '## Lean4 build', | ||
| '', | ||
| '`lake build` completed successfully for this change.', | ||
| '', | ||
| `Workflow: ${context.workflow} run [\`${context.runId}\`](${context.serverUrl}/${context.repo.owner}/${context.repo.repo}/actions/runs/${context.runId})` | ||
| ].join('\n'); | ||
| const { data: comments } = await github.rest.issues.listComments({ | ||
| owner: context.repo.owner, | ||
| repo: context.repo.repo, | ||
| issue_number: context.issue.number | ||
| }); | ||
| const marker = '<!-- specsync-lean4-ci -->'; | ||
| const existing = comments.find(c => c.body && c.body.includes(marker)); | ||
| const fullBody = marker + '\n' + body; | ||
| if (existing) { | ||
| await github.rest.issues.updateComment({ | ||
| owner: context.repo.owner, | ||
| repo: context.repo.repo, | ||
| comment_id: existing.id, | ||
| body: fullBody | ||
| }); | ||
| } else { | ||
| await github.rest.issues.createComment({ | ||
| owner: context.repo.owner, | ||
| repo: context.repo.repo, | ||
| issue_number: context.issue.number, | ||
| body: fullBody | ||
| }); | ||
| } | ||
