diff --git a/.github/workflows/main.yml b/.github/workflows/main.yml index 51ea2fd..6dd923b 100644 --- a/.github/workflows/main.yml +++ b/.github/workflows/main.yml @@ -46,54 +46,48 @@ jobs: cd hol-light git checkout c153f40da8deb3bcc7aaef39126ad15e4713e68c export HOLLIGHT_DIR=`pwd` - make eval `opam env` + make hol2dk patch - name: Dump proofs run: | - eval `opam env` cp xci.ml hol-light/ cd hol-light + eval `opam env` hol2dk dump-simp-use xci.ml - name: Test single-threaded dk output run: | - eval `opam env` - export HOL2DK_DIR=`pwd` cd hol-light ln -s ../theory_hol.dk + eval `opam env` hol2dk xci.dk dk check xci.dk - name: Test single-threaded lp output run: | - eval `opam env` - export HOL2DK_DIR=`pwd` cd hol-light + eval `opam env` 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` cd hol-light + eval `opam env` 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` cd hol-light + eval `opam env` 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 + eval `opam env` hol2dk link xci make split make -j3 lp