test.yml

name: Test
on: [push]
jobs:
  Test:
    runs-on: ubuntu-latest
    steps:
      - name: Check out repository code
        uses: actions/checkout@v3

      - name: Install elan & Lean
        run: |
          set -o pipefail
          curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh -s -- --default-toolchain none -y
          ~/.elan/bin/lean --version
          echo "$HOME/.elan/bin" >> $GITHUB_PATH

      - name: Download TPTP
        run: |
          set -o pipefail
          wget https://www.tptp.org/TPTP/Archive/TPTP-v8.0.0.tgz
          tar -zxvf TPTP-v8.0.0.tgz -C ..

      - name: lake build
        run: |
          set -o pipefail
          lake build
      
      - name: Test THF
        run: |
          export LEAN_PATH=./build/lib
          while read p; do
            echo "THF Problem: $p"
            echo "import Duper.TPTP import Duper.Tactic set_option inhabitationReasoning false tptp ${p:0:6} \"../TPTP-v8.0.0/Problems/${p:0:3}/$p.p\" by duper_no_timing"\
              | lake env ~/.elan/bin/lean -R ./. -o ./build/myfile.olean -i ./build/myfile.ilean --stdin --load-dynlib ./build/lib/libDuper-Tactic-1.so || true
          done <./.github/thf_tests.txt

      - name: Test TFF
        run: |
          export LEAN_PATH=./build/lib
          while read p; do
            echo "TFF Problem: $p"
            echo "import Duper.TPTP import Duper.Tactic set_option inhabitationReasoning false tptp ${p:0:6} \"../TPTP-v8.0.0/Problems/${p:0:3}/$p.p\" by duper_no_timing"\
              | lake env ~/.elan/bin/lean -R ./. -o ./build/myfile.olean -i ./build/myfile.ilean --stdin --load-dynlib ./build/lib/libDuper-Tactic-1.so || true
          done <./.github/tff_tests.txt

      - name: Test FOF
        run: |
          export LEAN_PATH=./build/lib
          while read p; do
            echo "FOF Problem: $p"
            echo "import Duper.TPTP import Duper.Tactic set_option inhabitationReasoning false tptp ${p:0:6} \"../TPTP-v8.0.0/Problems/${p:0:3}/$p.p\" have inhabitedIota : Inhabited TPTP.iota := sorry; by duper_no_timing"\
              | lake env ~/.elan/bin/lean -R ./. -o ./build/myfile.olean -i ./build/myfile.ilean --stdin --load-dynlib ./build/lib/libDuper-Tactic-1.so || true
          done <./.github/fof_tests.txt