Skip to content

Add example for Coq #3327

Add example for Coq

Add example for Coq #3327

Workflow file for this run

name: Test Workspace
on:
push:
branches: [main]
pull_request:
merge_group:
workflow_dispatch:
concurrency:
group: ${{ github.workflow }}-${{ github.ref }}
cancel-in-progress: true
jobs:
test-workspace:
strategy:
fail-fast: false
matrix:
os:
- macos-latest
- ubuntu-latest
- windows-latest
runs-on: ${{ matrix.os }}
steps:
- uses: actions/checkout@v4
- uses: Swatinem/rust-cache@v2
- name: Test
run: cargo test --workspace --exclude hax-engine-names-extract --verbose
- name: Test `hax-frontend-exporter` with feature `rustc` off
run: cargo check -p hax-frontend-exporter --no-default-features --verbose
no-std-lib:
runs-on: ubuntu-latest
steps:
- uses: dtolnay/rust-toolchain@master
with:
toolchain: stable
targets: thumbv7em-none-eabi
- uses: actions/checkout@v4
- uses: Swatinem/rust-cache@v2
- name: Build no-std
run: |
rustup target add thumbv7em-none-eabi
cargo build -p hax-lib --target thumbv7em-none-eabi