Bump koffi from 2.16.3 to 3.1.6 in /bindings/nodejs #112
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: Formal Verification | ||
| on: | ||
| push: | ||
| branches: [main, develop] | ||
| pull_request: | ||
| branches: [main] | ||
| schedule: | ||
| - cron: "0 2 * * *" | ||
| jobs: | ||
| formal-verify: | ||
| runs-on: ubuntu-latest | ||
| permissions: | ||
| contents: read | ||
| steps: | ||
| - name: Checkout code | ||
| uses: actions/checkout@v4 | ||
| - name: Setup Lean 4 | ||
| uses: leanprover/lean-action@v1 | ||
| - name: Setup Python | ||
| uses: actions/setup-python@v5 | ||
| with: | ||
| python-version: "3.11" | ||
| - name: Cache Lean dependencies | ||
| uses: actions/cache@v4 | ||
| with: | ||
| path: .lake | ||
| key: ${{ runner.os }}-lean-${{ hashFiles('lakefile.lean', 'lean-toolchain') }} | ||
| restore-keys: | | ||
| ${{ runner.os }}-lean- | ||
| # Lean warnings fail the build: `lakefile.lean` sets `-DwarningAsError=true`. | ||
| - name: Build Lean project | ||
| run: lake build | ||
| - name: Build Lean CLI targets | ||
| run: | | ||
| set -euo pipefail | ||
| lake build ModelAssetGuard | ||
| lake build quantbound tokenizertest verifyweights bitflipcorpus quantverify128 perfecthash benchmarks tests | ||
| - name: Run Lean tests | ||
| run: lake exe tests | ||
| - name: Axiom inventory gate | ||
| run: | | ||
| python scripts/check_axioms.py | ||
| echo "Formal completeness is NOT claimed; see docs/axioms.md" | ||
| - name: Check for sorry statements | ||
| run: | | ||
| echo "Checking for incomplete proofs (sorry statements)" | ||
| SORRY_COUNT=$(python - <<'PY' | ||
| import pathlib, re | ||
| count = 0 | ||
| for p in pathlib.Path("src/lean").rglob("*.lean"): | ||
| count += len(re.findall(r"\bsorry\b", p.read_text(encoding="utf-8"))) | ||
| print(count) | ||
| PY | ||
| ) | ||
| echo "Found $SORRY_COUNT sorry statements" | ||
| test "$SORRY_COUNT" -eq 0 | ||
| echo "SORRY_COUNT=$SORRY_COUNT" >> "$GITHUB_ENV" | ||
| - name: Generate verification report | ||
| run: | | ||
| AXIOM_COUNT=$(python - <<'PY' | ||
| import re | ||
| from pathlib import Path | ||
| text = Path("docs/axioms.md").read_text(encoding="utf-8") | ||
| m = re.search(r"\*\*Count:\*\*\s*(\d+)\s*axioms", text) | ||
| print(m.group(1) if m else "?") | ||
| PY | ||
| ) | ||
| cat > verification_report.md << EOF | ||
| # Formal Verification Report | ||
| **Date:** $(date -u) | ||
| **Commit:** ${{ github.sha }} | ||
| **Branch:** ${{ github.ref_name }} | ||
| ## What this job checks | ||
| - Lean package builds with \`warningAsError\` | ||
| - Lean CLI targets build | ||
| - \`lake exe tests\` passes | ||
| - \`sorry\` count is zero | ||
| - Axiom inventory matches \`docs/axioms.md\` (count: ${AXIOM_COUNT}) | ||
| ## What this job does NOT claim | ||
| - Formal completeness | ||
| - That Float / opaque obligation markers are proven theorems | ||
| - That runtime CLIs are proven correct in Lean (they delegate to Rust) | ||
| See \`docs/axioms.md\` for the explicit axiom list. | ||
| EOF | ||
| echo "Report generated: verification_report.md" | ||
| - name: Upload verification report | ||
| uses: actions/upload-artifact@v4 | ||
| with: | ||
| name: formal-verification-report | ||
| path: verification_report.md | ||
| - name: Comment on PR | ||
| if: github.event_name == 'pull_request' | ||
| uses: actions/github-script@v7 | ||
| with: | ||
| script: | | ||
| const fs = require('fs'); | ||
| const report = fs.readFileSync('verification_report.md', 'utf8'); | ||
| github.rest.issues.createComment({ | ||
| issue_number: context.issue.number, | ||
| owner: context.repo.owner, | ||
| repo: context.repo.repo, | ||
| body: `## Formal verification job\n\n${report}` | ||
| }); | ||
