valence-shell/.github/workflows/rust-cli.yml at 85d8eb5f8aab7639c331e2054da7a7977a872e81 · hyperpolymath/valence-shell · GitHub

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
# 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@7e35be21c2b94d972b1143087fabc27d7dc881ef  # 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@7e35be21c2b94d972b1143087fabc27d7dc881ef  # 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