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.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
          ./patch hol-light
      - name: Dump proofs
        run: |
          eval `opam env`
          cd hol-light; hol2dk dump ../xci.ml
      - name: Generate and check single-threaded dk output
        run: |
          eval `opam env`
          hol2dk pos xci
          hol2dk xci.dk
          dk check xci.dk
      - name: Generate and check single-threaded lp output
        run: |
          eval `opam env`
          hol2dk pos xci
          hol2dk xci.lp
          lambdapi check --lib-root=. --map-dir=hol-light:. xci.lp
      - name: Generate and check multi-threaded dk output
        run: |
          eval `opam env`
          hol2dk dg 3 xci
          hol2dk mk 3 xci .
          make -j 3 -f xci.mk dk
          dk check xci.dk
      - name: Generate and check multi-threaded lp output
        run: |
          eval `opam env`
          make -j 3 -f xci.mk lp
          lambdapi check --lib-root=. --map-dir=hol-light:. xci.lp