ci: harden workflows — timeout caps, pinned+verified elan, drop empty… #145
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: MPL-2.0 | |
| name: Rust CLI Tests | |
| on: | |
| push: | |
| paths: | |
| - 'impl/rust-cli/**' | |
| - 'proofs/lean4/**' | |
| - '.github/workflows/rust-cli.yml' | |
| pull_request: | |
| paths: | |
| - 'impl/rust-cli/**' | |
| - 'proofs/lean4/**' | |
| permissions: | |
| contents: read | |
| jobs: | |
| test: | |
| name: Test Rust CLI | |
| runs-on: ubuntu-latest | |
| timeout-minutes: 30 | |
| steps: | |
| - name: Checkout code | |
| uses: actions/checkout@9c091bb21b7c1c1d1991bb908d89e4e9dddfe3e0 # v4 | |
| - name: Install Rust toolchain | |
| uses: dtolnay/rust-toolchain@6d9817901c499d6b02debbb57edb38d33daa680b # stable | |
| with: | |
| components: rustfmt, clippy | |
| - name: Cache Rust dependencies | |
| uses: Swatinem/rust-cache@baf1a810e98b6a3001d0d7234864ed75a17c42fb # v2 | |
| with: | |
| workspaces: impl/rust-cli | |
| - name: Check formatting | |
| working-directory: impl/rust-cli | |
| run: cargo fmt --check | |
| - name: Run clippy | |
| working-directory: impl/rust-cli | |
| run: cargo clippy --all-targets --all-features -- -D warnings | |
| - name: Run unit tests | |
| working-directory: impl/rust-cli | |
| run: cargo test --lib --verbose | |
| - name: Run integration tests | |
| working-directory: impl/rust-cli | |
| run: cargo test --test integration_test --verbose | |
| - name: Run property tests | |
| working-directory: impl/rust-cli | |
| run: cargo test --test property_tests --verbose | |
| - name: Build release binary | |
| working-directory: impl/rust-cli | |
| run: cargo build --release | |
| - name: Verify binary works | |
| working-directory: impl/rust-cli | |
| run: | | |
| ./target/release/vsh --version | |
| echo "mkdir test_ci" | ./target/release/vsh | |
| lean4: | |
| name: Verify Lean 4 Proofs | |
| runs-on: ubuntu-latest | |
| timeout-minutes: 30 | |
| steps: | |
| - name: Checkout code | |
| uses: actions/checkout@9c091bb21b7c1c1d1991bb908d89e4e9dddfe3e0 # v4 | |
| - name: Install Lean 4 | |
| run: | | |
| # Download the elan installer pinned to an immutable release tag, | |
| # verify its SHA-256, then execute it — no `curl | sh`. | |
| curl -sSfL https://raw.githubusercontent.com/leanprover/elan/v3.1.1/elan-init.sh -o elan-init.sh | |
| echo "f5d473c923c093759ae3839073bec2a58e82cb8bc0e4083930e76090da75b310 elan-init.sh" | sha256sum -c - | |
| sh elan-init.sh -y --default-toolchain leanprover/lean4:v4.12.0 | |
| rm -f elan-init.sh | |
| echo "$HOME/.elan/bin" >> $GITHUB_PATH | |
| - name: Verify elan installation | |
| run: | | |
| lean --version | |
| lake --version | |
| - name: Build Lean proofs | |
| working-directory: proofs/lean4 | |
| run: lake build | |
| - name: Check for proof completeness | |
| working-directory: proofs/lean4 | |
| run: | | |
| # Count sorry placeholders (should be minimal) | |
| SORRY_COUNT=$(grep -r "sorry" *.lean | wc -l || echo "0") | |
| echo "Found $SORRY_COUNT sorry placeholders in proofs" | |
| # Note: Some sorry placeholders are expected during development |