align types used in the definition of real numbers #809
Workflow file for this run
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: [5.1.1, 4.14.1] | |
| camlp5-version: [8.02.01] | |
| dedukti-version: [2.7] | |
| lambdapi-version: [master, 2.5.0] | |
| dune-version: [3.15.0] | |
| runs-on: ubuntu-latest | |
| steps: | |
| # actions/checkout must be done BEFORE avsm/setup-ocaml | |
| - name: Checkout hol2dk | |
| uses: actions/checkout@v4 | |
| - 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 }} zarith 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: | | |
| eval `opam env` | |
| export HOL2DK_DIR=`pwd` | |
| export HOLLIGHT_DIR=`pwd`/hol-light | |
| git clone https://github.com/jrh13/hol-light | |
| cd hol-light | |
| git checkout | |
| make | |
| hol2dk patch | |
| - name: Dump proofs | |
| run: | | |
| eval `opam env` | |
| export HOL2DK_DIR=`pwd` | |
| export HOLLIGHT_DIR=`pwd`/hol-light | |
| cp xci.ml hol-light/ | |
| cd hol-light | |
| hol2dk dump-simp-before-hol xci.ml | |
| - name: Test single-threaded dk output | |
| run: | | |
| eval `opam env` | |
| export HOL2DK_DIR=`pwd` | |
| export HOLLIGHT_DIR=`pwd`/hol-light | |
| cd hol-light | |
| ln -s ../theory_hol.dk | |
| hol2dk xci.dk | |
| dk check xci.dk | |
| - name: Test single-threaded lp output | |
| run: | | |
| eval `opam env` | |
| export HOL2DK_DIR=`pwd` | |
| export HOLLIGHT_DIR=`pwd`/hol-light | |
| cd hol-light | |
| hol2dk xci.lp | |
| ln -s ../theory_hol.lp | |
| ln -s ../lambdapi.pkg | |
| lambdapi check xci.lp | |
| - name: Test multi-threaded dk output with mk | |
| run: | | |
| eval `opam env` | |
| export HOL2DK_DIR=`pwd` | |
| export HOLLIGHT_DIR=`pwd`/hol-light | |
| cd hol-light | |
| hol2dk mk 3 xci | |
| make -f xci.mk -j3 dk | |
| dk check xci.dk | |
| - name: Test multi-threaded lp output with mk | |
| run: | | |
| eval `opam env` | |
| export HOL2DK_DIR=`pwd` | |
| export HOLLIGHT_DIR=`pwd`/hol-light | |
| cd hol-light | |
| make -f xci.mk -j3 lp | |
| make -f xci.mk -j3 lpo | |
| - name: Test multi-threaded lp output with split | |
| run: | | |
| eval `opam env` | |
| export HOL2DK_DIR=`pwd` | |
| export HOLLIGHT_DIR=`pwd`/hol-light | |
| mkdir -p output/xci | |
| cd output/xci | |
| hol2dk link xci | |
| make split | |
| make -j3 lp | |
| make -j3 v | |
| make -j3 lpo | |
| # - name: Test --max-steps 1000 and --max-abbrevs 10000 | |
| # run: | | |
| # eval `opam env` | |
| # export HOL2DK_DIR=`pwd` | |
| # export HOLLIGHT_DIR=`pwd`/hol-light | |
| # cd output/xci | |
| # make clean-lp | |
| # make -j3 HOL2DK_OPTIONS='--max-steps 1000 --max-abbrevs 10000' lp | |
| # make -j3 lpo | |
| # - name: Test resize thm75360.lp 500 | |
| # run: | | |
| # eval `opam env` | |
| # export HOL2DK_DIR=`pwd` | |
| # export HOLLIGHT_DIR=`pwd`/hol-light | |
| # cd output/xci | |
| # make clean-lpo | |
| # hol2dk resize thm75360.lp 500 | |
| # make -j3 lpo | |
| # - name: Test resize thm75360.lp 100 | |
| # run: | | |
| # eval `opam env` | |
| # export HOL2DK_DIR=`pwd` | |
| # export HOLLIGHT_DIR=`pwd`/hol-light | |
| # cd output/xci | |
| # make clean-lpo | |
| # hol2dk resize thm75360.lp 100 | |
| # make -j3 lpo | |
| # - name: Test resize thm75360_term_abbrevs.lp 300 | |
| # run: | | |
| # eval `opam env` | |
| # export HOL2DK_DIR=`pwd` | |
| # export HOLLIGHT_DIR=`pwd`/hol-light | |
| # cd output/xci | |
| # make clean-lpo | |
| # hol2dk resize thm75360_term_abbrevs.lp 300 | |
| # make -j3 lpo | |
| # - name: Test resize thm75360_term_abbrevs.lp 100 | |
| # run: | | |
| # eval `opam env` | |
| # export HOL2DK_DIR=`pwd` | |
| # export HOLLIGHT_DIR=`pwd`/hol-light | |
| # cd output/xci | |
| # make clean-lpo | |
| # hol2dk resize thm75360_term_abbrevs.lp 100 | |
| # make -j3 lpo |