proof(formal): close preservation theorem — zero Admitted #50
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
| # SPDX-License-Identifier: PMPL-1.0-or-later | ||
|
Check failure on line 1 in .github/workflows/rust-ci.yml
|
||
| # Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk> | ||
| # | ||
| # rust-ci.yml — Cargo build, test, clippy, and fmt for Rust projects. | ||
| # Only runs if Cargo.toml exists in the repo root. | ||
| name: Rust CI | ||
| on: | ||
| pull_request: | ||
| branches: ['**'] | ||
| push: | ||
| branches: [main, master] | ||
| permissions: | ||
| contents: read | ||
| jobs: | ||
| check: | ||
| name: Cargo check + clippy + fmt | ||
| runs-on: ubuntu-latest | ||
| if: hashFiles('Cargo.toml') != '' | ||
| steps: | ||
| - name: Checkout repository | ||
| uses: actions/checkout@34e114876b0b11c390a56381ad16ebd13914f8d5 # v4 | ||
| - name: Install Rust toolchain | ||
| uses: dtolnay/rust-toolchain@4be9e76fd7c4901c61fb841f559994984270fce7 # stable | ||
| with: | ||
| components: clippy, rustfmt | ||
| - name: Cache cargo registry and build | ||
| uses: Swatinem/rust-cache@779680da715d629ac1d338a641029a2f4372abb5 # v2 | ||
| - name: Cargo check | ||
| run: cargo check --all-targets 2>&1 | ||
| - name: Cargo fmt | ||
| run: cargo fmt --all -- --check | ||
| - name: Cargo clippy | ||
| run: cargo clippy --all-targets -- -D warnings | ||
| test: | ||
| name: Cargo test | ||
| runs-on: ubuntu-latest | ||
| needs: check | ||
| if: hashFiles('Cargo.toml') != '' | ||
| steps: | ||
| - name: Checkout repository | ||
| uses: actions/checkout@34e114876b0b11c390a56381ad16ebd13914f8d5 # v4 | ||
| - name: Install Rust toolchain | ||
| uses: dtolnay/rust-toolchain@4be9e76fd7c4901c61fb841f559994984270fce7 # stable | ||
| - name: Cache cargo registry and build | ||
| uses: Swatinem/rust-cache@779680da715d629ac1d338a641029a2f4372abb5 # v2 | ||
| - name: Run tests | ||
| run: cargo test --all-targets | ||
| - name: Write summary | ||
| if: always() | ||
| run: | | ||
| echo "## Rust CI Results" >> "$GITHUB_STEP_SUMMARY" | ||
| echo "" >> "$GITHUB_STEP_SUMMARY" | ||
| echo "- **cargo check**: passed" >> "$GITHUB_STEP_SUMMARY" | ||
| echo "- **cargo test**: completed" >> "$GITHUB_STEP_SUMMARY" | ||
| status-gate: | ||
| name: Status gate | ||
| runs-on: ubuntu-latest | ||
| needs: check | ||
| if: hashFiles('Cargo.toml') != '' | ||
| steps: | ||
| - name: Checkout repository | ||
| uses: actions/checkout@34e114876b0b11c390a56381ad16ebd13914f8d5 # v4 | ||
| - name: Install Rust toolchain | ||
| uses: dtolnay/rust-toolchain@4be9e76fd7c4901c61fb841f559994984270fce7 # stable | ||
| - name: Cache cargo registry and build | ||
| uses: Swatinem/rust-cache@779680da715d629ac1d338a641029a2f4372abb5 # v2 | ||
| - name: Run status gate | ||
| run: ./scripts/status-gate.sh | ||
| proofs: | ||
| name: Coq proofs | ||
| runs-on: ubuntu-latest | ||
| needs: check | ||
| steps: | ||
| - name: Checkout repository | ||
| uses: actions/checkout@34e114876b0b11c390a56381ad16ebd13914f8d5 # v4 | ||
| - name: Install Coq | ||
| run: | | ||
| sudo apt-get update | ||
| sudo apt-get install -y coq | ||
| - name: Build Coq proofs | ||
| run: | | ||
| cd formal | ||
| coq_makefile -f _CoqProject -o Makefile | ||
| make | ||
