Bump pytest from 8.3.5 to 9.1.1 #31
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: CI | |
| on: | |
| push: | |
| branches: ["main", "master", "recovery/**", "feature/**", "fix/**", "test/**", "docs/**", "release/**"] | |
| pull_request: | |
| branches: ["main", "master", "recovery/**"] | |
| permissions: | |
| contents: read | |
| concurrency: | |
| group: ci-${{ github.workflow }}-${{ github.ref }} | |
| cancel-in-progress: true | |
| jobs: | |
| lean-build: | |
| runs-on: ubuntu-latest | |
| steps: | |
| - name: Checkout | |
| uses: actions/checkout@11bd71901bbe5b1630ceea73d27597364c9af683 # v4.2.2 | |
| - name: Lean build | |
| uses: leanprover/lean-action@38fbc41a8c28c4cbaec22d7f7de508ec2e7c0dd9 # v1 | |
| with: | |
| build: true | |
| lint: false | |
| lean-lint: | |
| runs-on: ubuntu-latest | |
| steps: | |
| - uses: actions/checkout@11bd71901bbe5b1630ceea73d27597364c9af683 # v4.2.2 | |
| - uses: leanprover/lean-action@38fbc41a8c28c4cbaec22d7f7de508ec2e7c0dd9 # v1 | |
| with: | |
| build: true | |
| lint: true | |
| prohibited-tactics: | |
| runs-on: ubuntu-latest | |
| steps: | |
| - uses: actions/checkout@11bd71901bbe5b1630ceea73d27597364c9af683 # v4.2.2 | |
| - uses: actions/setup-python@0b93645e9fea7318ecaed2b359559ac225c90a2b # v5.3.0 | |
| with: | |
| python-version: "3.11" | |
| - name: Prohibited tactic scan | |
| run: python scripts/scan_prohibited_tactics.py | |
| axiom-audit: | |
| runs-on: ubuntu-latest | |
| needs: [lean-build] | |
| steps: | |
| - uses: actions/checkout@11bd71901bbe5b1630ceea73d27597364c9af683 # v4.2.2 | |
| - uses: leanprover/lean-action@38fbc41a8c28c4cbaec22d7f7de508ec2e7c0dd9 # v1 | |
| with: | |
| build: true | |
| - uses: astral-sh/setup-uv@c771a70e6277c0a99b617c7a806ffedaca235ff9 # v9.0.0 | |
| with: | |
| python-version: "3.11" | |
| enable-cache: true | |
| - name: Sync frozen deps | |
| run: uv sync --frozen --all-extras | |
| - name: Generate concrete module for axiom audit | |
| run: | | |
| OUT_DIR="${RUNNER_TEMP}/lv-axiom-generated" | |
| mkdir -p "${OUT_DIR}" | |
| uv run leanverifier generate \ | |
| --model examples/affine_binary/model.json \ | |
| --request examples/affine_binary/request.json \ | |
| --out-dir "${OUT_DIR}" | |
| echo "GENERATED_DIR=${OUT_DIR}" >> "${GITHUB_ENV}" | |
| echo "GENERATED_FILE=$(ls "${OUT_DIR}"/GeneratedModel_*.lean | head -n 1)" >> "${GITHUB_ENV}" | |
| - name: Run axiom audit (library + generated) | |
| run: | | |
| uv run python scripts/audit_axioms.py \ | |
| --generated "${GENERATED_FILE}" \ | |
| --report "${RUNNER_TEMP}/axiom-report.txt" | |
| - name: Upload axiom report | |
| uses: actions/upload-artifact@65c4c4a1ddee5b72f698fdd19549f0f0fb45cf08 # v4.6.0 | |
| with: | |
| name: axiom-report | |
| path: ${{ runner.temp }}/axiom-report.txt | |
| lean4checker: | |
| runs-on: ubuntu-latest | |
| needs: [lean-build] | |
| steps: | |
| - uses: actions/checkout@11bd71901bbe5b1630ceea73d27597364c9af683 # v4.2.2 | |
| - uses: leanprover/lean-action@38fbc41a8c28c4cbaec22d7f7de508ec2e7c0dd9 # v1 | |
| with: | |
| build: true | |
| - name: lean4checker --fresh | |
| run: | | |
| chmod +x scripts/run_lean4checker.sh | |
| scripts/run_lean4checker.sh "${GITHUB_WORKSPACE}" \ | |
| "${RUNNER_TEMP}/axiom-report-lean4checker.txt" | |
| - name: Upload lean4checker report | |
| uses: actions/upload-artifact@65c4c4a1ddee5b72f698fdd19549f0f0fb45cf08 # v4.6.0 | |
| if: always() | |
| with: | |
| name: axiom-report-lean4checker | |
| path: ${{ runner.temp }}/axiom-report-lean4checker.txt | |
| python-unit: | |
| runs-on: ubuntu-latest | |
| steps: | |
| - uses: actions/checkout@11bd71901bbe5b1630ceea73d27597364c9af683 # v4.2.2 | |
| - uses: astral-sh/setup-uv@c771a70e6277c0a99b617c7a806ffedaca235ff9 # v9.0.0 | |
| with: | |
| python-version: "3.11" | |
| enable-cache: true | |
| - name: Sync frozen deps | |
| run: uv sync --frozen --all-extras | |
| - name: Ruff | |
| run: | | |
| uv run ruff check src/leanverifier tests scripts | |
| uv run ruff format --check src/leanverifier tests scripts | |
| - name: Mypy | |
| run: uv run mypy src/leanverifier | |
| - name: Pytest unit + coverage | |
| run: uv run python -m pytest tests/unit tests/schema --cov=src/leanverifier --cov-fail-under=70 | |
| schema-negative: | |
| runs-on: ubuntu-latest | |
| steps: | |
| - uses: actions/checkout@11bd71901bbe5b1630ceea73d27597364c9af683 # v4.2.2 | |
| - uses: astral-sh/setup-uv@c771a70e6277c0a99b617c7a806ffedaca235ff9 # v9.0.0 | |
| with: | |
| python-version: "3.11" | |
| enable-cache: true | |
| - run: uv sync --frozen --all-extras | |
| - run: uv run python -m pytest tests/schema -m schema -k negative | |
| generator-determinism: | |
| runs-on: ubuntu-latest | |
| steps: | |
| - uses: actions/checkout@11bd71901bbe5b1630ceea73d27597364c9af683 # v4.2.2 | |
| - uses: astral-sh/setup-uv@c771a70e6277c0a99b617c7a806ffedaca235ff9 # v9.0.0 | |
| with: | |
| python-version: "3.11" | |
| enable-cache: true | |
| - run: uv sync --frozen --all-extras | |
| - run: uv run python -m pytest tests/unit/test_generator_determinism.py -m unit | |
| verify-positive: | |
| runs-on: ubuntu-latest | |
| needs: [lean-build] | |
| steps: | |
| - uses: actions/checkout@11bd71901bbe5b1630ceea73d27597364c9af683 # v4.2.2 | |
| - uses: leanprover/lean-action@38fbc41a8c28c4cbaec22d7f7de508ec2e7c0dd9 # v1 | |
| with: | |
| build: true | |
| - uses: astral-sh/setup-uv@c771a70e6277c0a99b617c7a806ffedaca235ff9 # v9.0.0 | |
| with: | |
| python-version: "3.11" | |
| enable-cache: true | |
| - run: uv sync --frozen --all-extras | |
| - name: Positive verify + inspect (markers, not -k alone) | |
| run: uv run python -m pytest tests/integration -m "positive and lean" --maxfail=1 | |
| integration-negative: | |
| runs-on: ubuntu-latest | |
| steps: | |
| - uses: actions/checkout@11bd71901bbe5b1630ceea73d27597364c9af683 # v4.2.2 | |
| - uses: astral-sh/setup-uv@c771a70e6277c0a99b617c7a806ffedaca235ff9 # v9.0.0 | |
| with: | |
| python-version: "3.11" | |
| enable-cache: true | |
| - run: uv sync --frozen --all-extras | |
| - run: uv run python -m pytest tests/integration -m "negative" | |
| mutation: | |
| runs-on: ubuntu-latest | |
| needs: [lean-build] | |
| steps: | |
| - uses: actions/checkout@11bd71901bbe5b1630ceea73d27597364c9af683 # v4.2.2 | |
| - uses: leanprover/lean-action@38fbc41a8c28c4cbaec22d7f7de508ec2e7c0dd9 # v1 | |
| with: | |
| build: true | |
| - uses: astral-sh/setup-uv@c771a70e6277c0a99b617c7a806ffedaca235ff9 # v9.0.0 | |
| with: | |
| python-version: "3.11" | |
| enable-cache: true | |
| - run: uv sync --frozen --all-extras | |
| - name: Mutation table (verify/audit/inspect) | |
| run: uv run python -m pytest tests/mutation -m mutation --maxfail=1 | |
| security-tests: | |
| runs-on: ubuntu-latest | |
| steps: | |
| - uses: actions/checkout@11bd71901bbe5b1630ceea73d27597364c9af683 # v4.2.2 | |
| - uses: astral-sh/setup-uv@c771a70e6277c0a99b617c7a806ffedaca235ff9 # v9.0.0 | |
| with: | |
| python-version: "3.11" | |
| enable-cache: true | |
| - run: uv sync --frozen --all-extras | |
| - run: uv run python -m pytest tests/security -m security | |
| security-windows: | |
| runs-on: windows-latest | |
| steps: | |
| - uses: actions/checkout@11bd71901bbe5b1630ceea73d27597364c9af683 # v4.2.2 | |
| - uses: astral-sh/setup-uv@c771a70e6277c0a99b617c7a806ffedaca235ff9 # v9.0.0 | |
| with: | |
| python-version: "3.11" | |
| enable-cache: true | |
| - run: uv sync --frozen --all-extras | |
| - name: Security suite on Windows | |
| run: uv run python -m pytest tests/security -m security | |
| docs-claims: | |
| runs-on: ubuntu-latest | |
| steps: | |
| - uses: actions/checkout@11bd71901bbe5b1630ceea73d27597364c9af683 # v4.2.2 | |
| - uses: astral-sh/setup-uv@c771a70e6277c0a99b617c7a806ffedaca235ff9 # v9.0.0 | |
| with: | |
| python-version: "3.11" | |
| enable-cache: true | |
| - run: uv sync --frozen --all-extras | |
| - run: uv run python scripts/verify_docs.py --mode claims | |
| docs-links: | |
| runs-on: ubuntu-latest | |
| steps: | |
| - uses: actions/checkout@11bd71901bbe5b1630ceea73d27597364c9af683 # v4.2.2 | |
| - uses: astral-sh/setup-uv@c771a70e6277c0a99b617c7a806ffedaca235ff9 # v9.0.0 | |
| with: | |
| python-version: "3.11" | |
| enable-cache: true | |
| - run: uv sync --frozen --all-extras | |
| - run: uv run python scripts/verify_docs.py --mode links | |
| docs-commands: | |
| runs-on: ubuntu-latest | |
| needs: [lean-build] | |
| steps: | |
| - uses: actions/checkout@11bd71901bbe5b1630ceea73d27597364c9af683 # v4.2.2 | |
| - uses: leanprover/lean-action@38fbc41a8c28c4cbaec22d7f7de508ec2e7c0dd9 # v1 | |
| with: | |
| build: true | |
| - uses: astral-sh/setup-uv@c771a70e6277c0a99b617c7a806ffedaca235ff9 # v9.0.0 | |
| with: | |
| python-version: "3.11" | |
| enable-cache: true | |
| - run: uv sync --frozen --all-extras | |
| - name: Execute README/user-guide CLI commands | |
| run: uv run python scripts/verify_docs.py --mode commands | |
| wheel-smoke: | |
| runs-on: ubuntu-latest | |
| needs: [lean-build] | |
| steps: | |
| - uses: actions/checkout@11bd71901bbe5b1630ceea73d27597364c9af683 # v4.2.2 | |
| - uses: leanprover/lean-action@38fbc41a8c28c4cbaec22d7f7de508ec2e7c0dd9 # v1 | |
| with: | |
| build: true | |
| - uses: astral-sh/setup-uv@c771a70e6277c0a99b617c7a806ffedaca235ff9 # v9.0.0 | |
| with: | |
| python-version: "3.11" | |
| enable-cache: true | |
| - name: Sync frozen deps | |
| run: uv sync --frozen --all-extras | |
| - name: Build wheel and sdist | |
| run: uv build | |
| - name: Smoke install from /tmp with verify | |
| run: | | |
| uv run python scripts/smoke_wheel.py --dist dist --artifact both --require-verify | |
| docker-build: | |
| runs-on: ubuntu-latest | |
| steps: | |
| - uses: actions/checkout@11bd71901bbe5b1630ceea73d27597364c9af683 # v4.2.2 | |
| - name: Build Lean-only Docker image | |
| run: docker build -t leanverifier:ci . | |
| - name: Run formal checks in container | |
| run: | | |
| docker run --rm leanverifier:ci lake build | |
| docker run --rm --entrypoint lake leanverifier:ci env lean LeanVerifier/Audit/PublicAxioms.lean | |
| clean-worktree: | |
| runs-on: ubuntu-latest | |
| steps: | |
| - uses: actions/checkout@11bd71901bbe5b1630ceea73d27597364c9af683 # v4.2.2 | |
| - uses: leanprover/lean-action@38fbc41a8c28c4cbaec22d7f7de508ec2e7c0dd9 # v1 | |
| with: | |
| build: true | |
| lint: false | |
| - uses: astral-sh/setup-uv@c771a70e6277c0a99b617c7a806ffedaca235ff9 # v9.0.0 | |
| with: | |
| python-version: "3.11" | |
| enable-cache: true | |
| - name: Sync frozen deps | |
| run: uv sync --frozen --all-extras | |
| - name: Pytest (unit + schema subset) | |
| run: uv run python -m pytest tests/unit tests/schema -q | |
| - name: Axiom audit | |
| run: uv run python scripts/audit_axioms.py | |
| - name: Prohibited tactic scan | |
| run: python scripts/scan_prohibited_tactics.py | |
| - name: Docs verify (claims + links) | |
| run: | | |
| uv run python scripts/verify_docs.py --mode claims | |
| uv run python scripts/verify_docs.py --mode links | |
| - name: Generate outside checkout | |
| run: | | |
| OUT_DIR="${RUNNER_TEMP}/lv-clean-worktree-generate" | |
| mkdir -p "${OUT_DIR}" | |
| uv run leanverifier generate \ | |
| --model examples/affine_binary/model.json \ | |
| --request examples/affine_binary/request.json \ | |
| --out-dir "${OUT_DIR}" | |
| - name: Worktree remains clean | |
| run: test -z "$(git status --porcelain)" |