-
Notifications
You must be signed in to change notification settings - Fork 22
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
- Loading branch information
Showing
1 changed file
with
29 additions
and
26 deletions.
There are no files selected for viewing
This file contains 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
Original file line number | Diff line number | Diff line change |
---|---|---|
|
@@ -5,45 +5,48 @@ jobs: | |
build: | ||
runs-on: ubuntu-latest | ||
container: | ||
image: coqorg/coq:8.18.0-ocaml-4.14.2-flambda | ||
permissions: | ||
contents: write | ||
image: coqorg/base:5.0.0 # coqorg/coq:8.18.0-ocaml-5.0.0 | ||
# permissions: | ||
# contents: write | ||
steps: | ||
- name: nodejs install | ||
run: | | ||
sudo apt update | ||
sudo apt install nodejs npm jq -y | ||
node -v | ||
npm -v | ||
- name: Checkout code | ||
uses: actions/checkout@v3 | ||
# 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 | ||
- uses: dtolnay/[email protected] | ||
- run: cargo install --path cli/driver && cargo install --path cli/subcommands | ||
# curl --proto '=https' --tlsv1.2 -sSf https://sh.rustup.rs | sh | ||
# . "$HOME/.cargo/env" | ||
- name: jq install | ||
run: sudo apt update && sudo apt install jq -y | ||
- name: opam setup | ||
run: | | ||
export HOME=/home/coq | ||
export PATH=$HOME/.cargo/bin:$PATH | ||
env | ||
opam switch 4.14.2+flambda | ||
# export HOME=/home/coq | ||
# export PATH=$HOME/.cargo/bin:$PATH | ||
# env | ||
opam switch 5.0.0 | ||
eval $(opam env) | ||
- name: opam switch | ||
run: | | ||
opam switch | ||
opam list | ||
opam install coq -y | ||
opam install coq-record-update -y | ||
- name: Checkout code | ||
uses: actions/checkout@v3 | ||
- 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 | ||
run: ./setup.sh | ||
# - run: | | ||
# opam exec -- dune build -j 1 | ||
# opam exec -- dune install | ||
# working-directory: engine | ||
- name: Build | ||
working-directory: examples/coverage | ||
run: | | ||
curl -sL https://deb.nodesource.com/setup_16.x -o /tmp/nodesource_setup.sh | ||
sudo bash /tmp/nodesource_setup.sh | ||
# curl -sL https://deb.nodesource.com/setup_16.x -o /tmp/nodesource_setup.sh | ||
# sudo bash /tmp/nodesource_setup.sh | ||
cargo hax into coq | ||
cd proofs/coq/extraction | ||
sed 's/_impl_f_/_f_/' < Coverage_Test_instance.v > Coverage_Test_instance.v | ||
|