chore(licence): normalise to MPL-2.0 + CC-BY-SA-4.0 (canonical pair) #58
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 | |
| steps: | |
| - name: Checkout code | |
| uses: actions/checkout@9c091bb21b7c1c1d1991bb908d89e4e9dddfe3e0 # v4 | |
| - name: Install Lean 4 | |
| run: | | |
| curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh -s -- -y | |
| 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@27d5ce7f107fe9357f9df03efb73ab90386fccae # 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 |