Skip to content

wip

wip #13

Workflow file for this run

name: CI
on:
push:
pull_request:
env:
CARGO_TERM_COLOR: always
HAX_TOOLCHAIN: nightly-2025-11-08
CARGO_INSTALL_ROOT: ~/.cargo
CARGO_TARGET_DIR: ~/.cargo/ci-target
jobs:
rust_and_hax:
runs-on: ubuntu-latest
steps:
- uses: actions/checkout@v4
# ----- Rust stable for the crate -----
- name: Install Rust (stable)
uses: dtolnay/rust-toolchain@stable
- name: Rust cache (workspace)
uses: Swatinem/rust-cache@v2
with:
workspaces: |
rust/merkle_root_rs
- name: Build & test (Rust)
working-directory: rust/merkle_root_rs
run: |
cargo build --verbose
cargo test --verbose
# ----- Install pinned nightly for hax -----
- name: Install Rust toolchain for hax (pinned nightly)
uses: dtolnay/rust-toolchain@master
with:
toolchain: ${{ env.HAX_TOOLCHAIN }}
components: rustc-dev, llvm-tools-preview, rust-src, rustfmt, rust-analysis
- name: Cache cargo tools
uses: actions/cache@v4
with:
path: |
~/.cargo/bin
~/.cargo/registry
~/.cargo/git
~/.cargo/ci-target
key: ${{ runner.os }}-cargo-tools-${{ env.HAX_TOOLCHAIN }}-hax-0.3.5
- name: Install hax toolchain (pinned nightly) [WIP]
continue-on-error: true
env:
RUSTUP_TOOLCHAIN: ${{ env.HAX_TOOLCHAIN }}
run: |
rustc --version
cargo --version
cargo install cargo-hax --version 0.3.5 --locked
cargo install hax-driver --version 0.3.5 --locked
cargo install hax-rust-engine --version 0.3.5 --locked
cargo install hax-engine-names-extract --version 0.3.5 --locked
cargo install hax-export-json-schemas --version 0.3.5 --locked
which cargo-hax
which driver-hax-frontend-exporter
- name: Run hax extraction (pinned nightly) [WIP]
continue-on-error: true
env:
RUSTUP_TOOLCHAIN: ${{ env.HAX_TOOLCHAIN }}
run: |
./scripts/extract.sh
lean_optional_wip:
runs-on: ubuntu-latest
continue-on-error: true
steps:
- uses: actions/checkout@v4
- name: Install elan (Lean toolchain manager)
run: |
curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh -s -- -y
echo "$HOME/.elan/bin" >> $GITHUB_PATH
- name: Lean cache
uses: actions/cache@v4
with:
path: |
~/.elan
lean/.lake
key: ${{ runner.os }}-lean-${{ hashFiles('lean-toolchain', 'lean/lean-toolchain', 'lean/lakefile.toml', 'lean/lake-manifest.json') }}
restore-keys: |
${{ runner.os }}-lean-
- name: Build Lean (WIP, allowed to fail)
working-directory: lean
continue-on-error: true
run: |
lake update
lake build