Skip to content

feat(book): allow F* extraction + TC from within the book #2934

feat(book): allow F* extraction + TC from within the book

feat(book): allow F* extraction + TC from within the book #2934

Workflow file for this run

name: Test installations
on:
pull_request:
merge_group:
workflow_dispatch:
push:
branches: [main]
jobs:
docker:
if: ${{ github.event_name == 'workflow_dispatch' || github.event_name == 'merge_group' }}
runs-on: ubuntu-latest
steps:
- uses: actions/checkout@v3
- run: docker build -f .docker/Dockerfile . -t hax
setup_sh:
if: ${{ github.event_name == 'workflow_dispatch' || github.event_name == 'merge_group' }}
strategy:
matrix:
os:
- ubuntu-latest
- ubuntu-20.04
- macos-latest
- macos-12
runs-on: ${{ matrix.os }}
steps:
- uses: actions/checkout@v3
- if: runner.os == 'macOS'
run: brew install opam nodejs rustup-init jq
- if: runner.os == 'Linux'
run: sudo apt-get update
- if: runner.os == 'Linux'
run: sudo apt-get install -y opam nodejs jq
- run: curl --proto '=https' --tlsv1.3 https://sh.rustup.rs -sSf | sh -s -- -y
- run: opam init --bare -y && opam switch create -y 4.14.1
- name: Run `setup.sh`
run: |
export OPAMERRLOGLEN=0
./setup.sh
- run: cargo hax --version
- name: Test an extraction
run: |
cd examples/chacha20
eval $(opam env)
cargo hax into fstar
setup_sh_status:
if: |
always() &&
github.event_name == 'workflow_dispatch' ||github.event_name == 'merge_group'
needs: setup_sh
runs-on: ubuntu-latest
steps:
- name: Successful
if: ${{ !(contains(needs.*.result, 'failure')) }}
run: exit 0
- name: Failing
if: ${{ contains(needs.*.result, 'failure') }}
run: exit 1