main.yml

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.02.01]
        dedukti-version: [2.7]
        lambdapi-version: [master]
        dune-version: [3.14.2]
    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 }} 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: |
          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 c153f40da8deb3bcc7aaef39126ad15e4713e68c
          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-use 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