extend mapping to ZRECSPACE and the types recspace and option (#77) #353
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
| on: | |
| pull_request: | |
| types: [opened, synchronize, edited, reopened] | |
| push: | |
| workflow_dispatch: | |
| jobs: | |
| hol-light-to-dedukti: | |
| strategy: | |
| fail-fast: false | |
| matrix: | |
| ocaml-version: [4.14.1] | |
| camlp5-version: [8.00.05] | |
| dedukti-version: [2.7] | |
| lambdapi-version: [master] | |
| dune-version: [3.7.0] | |
| runs-on: ubuntu-latest | |
| steps: | |
| # actions/checkout must be done BEFORE avsm/setup-ocaml | |
| - name: Checkout hol2dk | |
| uses: actions/checkout@v3 | |
| - name: Install opam | |
| uses: avsm/setup-ocaml@v2 | |
| with: | |
| ocaml-compiler: ${{ matrix.ocaml-version }} | |
| - name: Install dune | |
| run: opam install -y dune.${{ matrix.dune-version }} | |
| - name: Compile hol2dk | |
| run: | | |
| eval `opam env` | |
| dune build | |
| dune install | |
| - name: Install hol-light dependencies, dedukti | |
| run: | | |
| sudo apt-get install -y libipc-system-simple-perl libstring-shellquote-perl | |
| opam install -y camlp5.${{ matrix.camlp5-version }} num ocamlfind dedukti.${{ matrix.dedukti-version }} #lambdapi.${{ matrix.lambdapi-version }} | |
| - name: Install lambdapi | |
| run: | | |
| git clone --depth 1 -b ${{ matrix.lambdapi-version }} https://github.com/Deducteam/lambdapi | |
| sudo apt-get install -y libev-dev | |
| opam pin lambdapi lambdapi | |
| opam install -y lambdapi | |
| - name: Get hol-light and patch it | |
| run: | | |
| git clone --depth 1 https://github.com/jrh13/hol-light | |
| eval `opam env` | |
| make -C hol-light | |
| export HOL2DK_DIR=. | |
| ./patch hol-light | |
| - name: Dump proofs | |
| run: | | |
| eval `opam env` | |
| cd hol-light; hol2dk dump-use-simp ../xci.ml; cd .. | |
| #hol2dk pos xci | |
| #hol2dk use xci | |
| #hol2dk simp xci | |
| - name: Generate and check single-threaded dk output | |
| run: | | |
| eval `opam env` | |
| hol2dk xci.dk | |
| dk check xci.dk | |
| - name: Generate and check single-threaded lp output | |
| run: | | |
| eval `opam env` | |
| hol2dk xci.lp | |
| lambdapi check xci.lp | |
| - name: Generate and check multi-threaded dk output | |
| run: | | |
| eval `opam env` | |
| hol2dk mk 3 xci | |
| export HOL2DK_DIR=. | |
| make -j 3 -f xci.mk dk | |
| dk check xci.dk | |
| - name: Generate and check multi-threaded lp output | |
| run: | | |
| eval `opam env` | |
| export HOL2DK_DIR=. | |
| make -j 3 -f xci.mk lp | |
| lambdapi check xci.lp |