main.yml

on:
  pull_request:
    types: [opened, synchronize, edited, reopened]
  push:
  workflow_dispatch:
jobs:
  hol-light-to-dedukti:
    strategy:
      fail-fast: false
      matrix:
        hol-light-version: [ea45176]
        ocaml-version: [4.14.2]
        camlp5-version: [8.02.01]
        dedukti-version: [2.7]
        lambdapi-version: [master, 2.5.1]
        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@v3
        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 ${{ matrix.hol-light-version }}
          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