Repository navigation
chore: estate standardization remainder — contractiles restructure, nix removal, Guix manifests, TruffleHog #65
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: Lean Verification Build | |
| on: | |
| push: | |
| branches: [main] | |
| paths: | |
| - 'proofs/lean4/**' | |
| - 'impl/rust-cli/src/proof_refs.rs' | |
| - '.github/workflows/lean-verification.yml' | |
| pull_request: | |
| paths: | |
| - 'proofs/lean4/**' | |
| - 'impl/ocaml/**' | |
| - 'impl/rust-cli/**' | |
| workflow_dispatch: | |
| permissions: | |
| contents: read | |
| jobs: | |
| build-lean-extraction: | |
| name: Build and Test Lean Extraction Pipeline | |
| 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 | |
| rm -f elan-init.sh | |
| echo "$HOME/.elan/bin" >> $GITHUB_PATH | |
| - name: Verify Lean installation | |
| run: | | |
| source $HOME/.elan/env | |
| lean --version | |
| lean --print-prefix | |
| ls -la $(lean --print-prefix)/lib/lean/libleanshared.so | |
| - name: Install Rust toolchain | |
| uses: dtolnay/rust-toolchain@6d9817901c499d6b02debbb57edb38d33daa680b | |
| with: | |
| toolchain: stable | |
| - name: Cache Lean build | |
| uses: actions/cache@55cc8345863c7cc4c66a329aec7e433d2d1c52a9 # v4 | |
| with: | |
| path: proofs/lean4/.lake | |
| key: ${{ runner.os }}-lean-${{ hashFiles('proofs/lean4/lakefile.lean', 'proofs/lean4/lean-toolchain') }} | |
| - name: Build Lean extraction | |
| run: | | |
| source $HOME/.elan/env | |
| cd proofs/lean4 | |
| lake build Extraction | |
| - name: Verify Lean extraction output | |
| run: | | |
| ls -lh proofs/lean4/.lake/build/ir/Extraction.c | |
| wc -l proofs/lean4/.lake/build/ir/Extraction.c | |
| - name: Build C wrapper library | |
| run: | | |
| source $HOME/.elan/env | |
| cd impl/ocaml | |
| lean_prefix="$(lean --print-prefix)" | |
| lean_include="$lean_prefix/include" | |
| lean_lib="$lean_prefix/lib/lean" | |
| gcc -shared -fPIC -o liblean_vsh.so \ | |
| lean_wrapper.c \ | |
| ../../proofs/lean4/.lake/build/ir/Extraction.c \ | |
| -I"$lean_include" \ | |
| -L"$lean_lib" \ | |
| -lleanshared \ | |
| -Wl,-rpath,"$lean_lib" | |
| - name: Verify shared library | |
| run: | | |
| ls -lh impl/ocaml/liblean_vsh.so | |
| ldd impl/ocaml/liblean_vsh.so | |
| nm -D impl/ocaml/liblean_vsh.so | grep vsh_safe || echo "Warning: vsh_safe functions not exported" | |
| - name: Cache Rust build | |
| uses: Swatinem/rust-cache@baf1a810e98b6a3001d0d7234864ed75a17c42fb # v2 | |
| with: | |
| workspaces: impl/rust-cli | |
| - name: Build Rust without Lean (baseline) | |
| run: | | |
| cd impl/rust-cli | |
| cargo build --release | |
| ls -lh target/release/vsh | |
| - name: Test Rust without Lean | |
| run: | | |
| cd impl/rust-cli | |
| cargo test | |
| cargo test --test correspondence_tests | |
| cargo test --test property_correspondence_tests | |
| - name: Report Rust binary size | |
| run: | | |
| echo "Rust binary: $(stat -c%s impl/rust-cli/target/release/vsh) bytes" | |
| - name: Upload artifacts | |
| uses: actions/upload-artifact@043fb46d1a93c77aae656e7c1c64a875d1fc6a0a # v7 | |
| with: | |
| name: lean-extraction-artifacts | |
| path: | | |
| proofs/lean4/.lake/build/ir/Extraction.c | |
| impl/ocaml/liblean_vsh.so | |
| impl/rust-cli/target/release/vsh |