revert #15
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
name: Coq Verification | |
on: | |
push: | |
branches: [ main ] | |
pull_request: | |
branches: [ main ] | |
jobs: | |
verify: | |
runs-on: ubuntu-latest | |
env: | |
OPAMYES: "1" | |
steps: | |
- name: Checkout code | |
uses: actions/checkout@v3 | |
- name: Install system dependencies | |
run: | | |
sudo apt-get update | |
sudo apt-get install -y opam git autoconf g++ m4 wget | |
- name: Initialize opam and create switch for Coq 8.14.1 | |
run: | | |
opam init --disable-sandboxing -y | |
opam switch create coq-8.14.1 --packages=coq.8.14.1 | |
eval $(opam env --switch=coq-8.14.1) | |
opam update -y | |
- name: Add Coq-released repository and install Coquelicot | |
run: | | |
opam repo add coq-released https://coq.inria.fr/opam/released --yes | |
opam update -y | |
opam install -y coq-coquelicot.3.2.0 | |
eval $(opam env --switch=coq-8.14.1) | |
- name: Run Coq Verification | |
run: | | |
eval $(opam env --switch=coq-8.14.1) | |
# Compile all Coq files in the 'coq' directory, | |
# mapping the physical directory 'coq' to the logical library 'UOR_H1_HPO' | |
find coq -name '*.v' -print0 | xargs -0 -n1 coqc -R coq UOR_H1_HPO |