main.yaml

on:
  pull_request:
    types: [opened, synchronize, edited, reopened]
  push:
  workflow_dispatch:
jobs:
  isabelle_dedukti:
    strategy:
      fail-fast: false
      matrix:
        ocaml-version: [4.14.1]
        dedukti-version: [2.7]
        lambdapi-version: [2.3.1]
        isabelle-version: [2022]
    runs-on: ubuntu-latest
    steps:
    # actions/checkout must be done BEFORE avsm/setup-ocaml
      - name: Checkout isabelle_dedukti
        uses: actions/checkout@v3
#      - name: Set up cache
#        id: cache
#        uses: actions/cache@v3
#        with:
#          path: |
#            ~/.isabelle
#            ~/kontroli-rs
#            ~/Isabelle${{ matrix.isabelle-version }}
#            ~/.opam
#          key: cache-${{ runner.os }}
      - name: Download Isabelle
#        if: steps.cache.outputs.cache-hit != 'true'
        run: |
          wget -q https://isabelle.in.tum.de/website-Isabelle${{ matrix.isabelle-version }}/dist/Isabelle${{ matrix.isabelle-version }}_linux.tar.gz
          tar -xzf Isabelle${{ matrix.isabelle-version }}_linux.tar.gz -C ~
      - name: Build isabelle_dedukti
        run: |
          ~/Isabelle${{ matrix.isabelle-version }}/bin/isabelle components -u .
          ~/Isabelle${{ matrix.isabelle-version }}/bin/isabelle scala_build
      - name: Patch Isabelle/HOL library
        run: |
          chmod -R +w ~/Isabelle${{ matrix.isabelle-version }}/src/HOL/
          patch -up0 -d ~/Isabelle${{ matrix.isabelle-version }}/src/HOL/ < HOL.patch
      - name: Install opam
#        if: steps.cache.outputs.cache-hit != 'true'
        uses: avsm/setup-ocaml@v2
        with:
          ocaml-compiler: ${{ matrix.ocaml-version }}
      - name: Install dkcheck
        run: opam install dedukti.${{ matrix.dedukti-version }}
      - name: Install lambdapi
        run: opam install lambdapi.${{ matrix.lambdapi-version }}
      - name: Install kocheck
        run: |
          cd ~
          git clone https://github.com/01mf02/kontroli-rs.git
          cd ~/kontroli-rs
          cargo install --path kocheck
      - name: Generate dk and lp outputs, check dk output for Pure
        run: |
          cd examples/
	  mkdir Pure/dkcheck Pure/lambdapi
          ~/Isabelle${{ matrix.isabelle-version }}/bin/isabelle build -b -d. Pure
          ~/Isabelle${{ matrix.isabelle-version }}/bin/isabelle dedukti_session -d. Pure
          cd Pure/dkcheck/
          eval $(opam env)
          bash dkcheck.sh
      # - name: Generate and check lp output for HOL.Groups
      #   run: |
      #     cp STTfa.dk STTfa.lp lambdapi.pkg examples/HOL.Groups
      #     cd examples/HOL.Groups
      #     ~/Isabelle${{ matrix.isabelle-version }}/bin/isabelle build -b -d. HOL.Groups_wp
      #     ~/Isabelle${{ matrix.isabelle-version }}/bin/isabelle dedukti_session -d. -l HOL.Groups_wp
      #     eval $(opam env)
      #     lambdapi check HOL_Groups.lp
      - name: Generate dk and lp outputs, check dk output for HOL.Groups
        run: |
          cd examples/
          mkdir HOL.Groups_wp/dkcheck HOL.Groups_wp/lambdapi
          ~/Isabelle${{ matrix.isabelle-version }}/bin/isabelle build -b -d. HOL.Groups_wp
          ~/Isabelle${{ matrix.isabelle-version }}/bin/isabelle dedukti_session -d. HOL.Groups_wp
          ~/Isabelle${{ matrix.isabelle-version }}/bin/isabelle dedukti_check -d. HOL.Groups_wp
          cd HOL.Groups_wp/dkcheck/
          eval $(opam env)
          bash dkcheck.sh
#          mkdir -p kocheck
#          ../../remove-requires.sh *.dk
#          cd kocheck
#          bash ../kocheck.sh
#          dk dep *.dk > deps.mk
#          make -f dedukti.mk