fix(ci): repair branch payload — remove invalid root-level timeout-mi… #153
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 all tests (unit + every integration suite + doctests) | |
| working-directory: impl/rust-cli | |
| run: cargo test --verbose | |
| - name: Run ffi/rust tests | |
| working-directory: ffi/rust | |
| run: cargo test --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 | |
| coverage: | |
| name: Code coverage (llvm-cov) | |
| 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: llvm-tools-preview | |
| - name: Cache Rust dependencies | |
| uses: Swatinem/rust-cache@baf1a810e98b6a3001d0d7234864ed75a17c42fb # v2 | |
| with: | |
| workspaces: impl/rust-cli | |
| - name: Install cargo-llvm-cov | |
| run: cargo install cargo-llvm-cov --locked | |
| - name: Measure coverage (impl/rust-cli) | |
| working-directory: impl/rust-cli | |
| run: | | |
| # Run the full suite once under instrumentation, then emit reports. | |
| # Measured and surfaced as a regression signal — not a hard gate. | |
| cargo llvm-cov --no-report | |
| cargo llvm-cov report --lcov --output-path lcov.info | |
| { | |
| echo '### Coverage — impl/rust-cli' | |
| echo '```' | |
| cargo llvm-cov report --summary-only | |
| echo '```' | |
| } >> "$GITHUB_STEP_SUMMARY" | |
| - name: Upload coverage (lcov) | |
| uses: actions/upload-artifact@043fb46d1a93c77aae656e7c1c64a875d1fc6a0a # v7 | |
| with: | |
| name: coverage-lcov | |
| path: impl/rust-cli/lcov.info |