fix: deep audit — fix all broken tests, real bugs, remove dead code, … #15
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: AGPL-3.0-or-later | |
| 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: read-all | |
| jobs: | |
| test: | |
| name: Test Rust CLI | |
| runs-on: ubuntu-latest | |
| steps: | |
| - name: Checkout code | |
| uses: actions/checkout@b4ffde65f46336ab88eb53be808477a3936bae11 # v4 | |
| - name: Install Rust toolchain | |
| uses: dtolnay/rust-toolchain@6d9817901c499d6b02debbb57edb38d33daa680b # stable | |
| with: | |
| components: rustfmt, clippy | |
| - name: Cache Rust dependencies | |
| uses: Swatinem/rust-cache@ad397744b0d591a723ab90405b7247fac0e6b8db # 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 | |
| steps: | |
| - name: Checkout code | |
| uses: actions/checkout@b4ffde65f46336ab88eb53be808477a3936bae11 # v4 | |
| - name: Install Lean 4 | |
| run: | | |
| curl -sSf https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh | sh -s -- -y --default-toolchain leanprover/lean4:v4.12.0 | |
| 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 |