lean4-ci.yml

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
              });
            }