Skip to content

Coq small fixes

Coq small fixes #18

name: Extract and Run - Coq
on: [pull_request]
jobs:
build:
runs-on: ubuntu-latest
container:
image: coqorg/base:5.0.0 # coqorg/coq:8.18.0-ocaml-5.0.0
options: --user root
# permissions:
# contents: write
steps:
- name: Checkout code
uses: actions/checkout@v4
# - name: Setup
# run: mkdir -m 1777 /__w
- name: env
run: |
export HOME=/home/coq
export PATH=$HOME/.cargo/bin:$PATH
env
- name: nodejs install
run: |
# curl -o- https://raw.githubusercontent.com/nvm-sh/nvm/v0.40.1/install.sh | bash
# . "$HOME/.nvm/nvm.sh"
# nvm -v
# nvm install node
# node -v
# npm -v
sudo apt update && sudo apt install nodejs -y
- name: install rust
# uses: Swatinem/rust-cache@v2
# uses: dtolnay/[email protected]
run: |
curl --proto '=https' --tlsv1.2 -sSf https://sh.rustup.rs | bash -s -- -y
. "$HOME/.cargo/env"
- name: jq install
run: sudo apt update && sudo apt install jq -y
- name: opam setup
run: |
opam switch 5.0.0
eval $(opam env)
opam install coq -y
opam install coq-record-update -y
- run: opam install . --verbose --deps-only -y
working-directory: engine
- name: Build
run: ./setup.sh
# - run: |
# opam exec -- dune build -j 1
# opam exec -- dune install
# working-directory: engine
- name: Build
working-directory: examples/coverage
run: |
cargo hax into coq
cd proofs/coq/extraction
sed 's/_impl_f_/_f_/' < Coverage_Test_instance.v > Coverage_Test_instance.v
coq_makefile -f _CoqProject -o Makefile
make