Remove some redundancy in the proof for presup #70
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: CI build | |
| on: | |
| push: | |
| branches: | |
| - main | |
| pull_request: | |
| branches: | |
| - main | |
| env: | |
| OCAML_VER: "4.14.0" | |
| COQ_VER: "8.17.1" | |
| jobs: | |
| wf: | |
| name: Completeness of _CoqProject | |
| runs-on: ubuntu-latest | |
| steps: | |
| - name: repo checkout | |
| uses: actions/checkout@v3 | |
| - name: check | |
| run: | | |
| .github/scripts/check_projects.sh theories | |
| build: | |
| name: Continuous Intergration | |
| runs-on: ubuntu-latest | |
| steps: | |
| - name: repo checkout | |
| uses: actions/checkout@v3 | |
| - name: setup OCaml | |
| uses: ocaml/setup-ocaml@v2 | |
| with: | |
| ocaml-compiler: ${{ env.OCAML_VER }} | |
| dune-cache: true | |
| - name: install Menhir and Coq | |
| run: | | |
| opam update | |
| opam install menhir | |
| opam pin add coq "${{ env.COQ_VER }}" | |
| - name: install Coq dependencies | |
| run: | | |
| opam repo add coq-released https://coq.inria.fr/opam/released | |
| opam update | |
| opam install coq-equations | |
| opam install coq-menhirlib | |
| opam install ppx_inline_test | |
| env: | |
| OPAMYES: "true" | |
| - name: build lib | |
| run: | | |
| eval $(opam env) | |
| cd theories/ | |
| make | |
| - name: test parser | |
| run: | | |
| eval $(opam env) | |
| dune build | |
| dune runtest |