Skip to content

ignoreUsableFacts option bug fix #233

ignoreUsableFacts option bug fix

ignoreUsableFacts option bug fix #233

Workflow file for this run

name: Test Executable
on: [push]
jobs:
TestExe:
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: |
while read p; do
echo "THF Problem: $p"
timeout 30 ./build/bin/duper "../TPTP-v8.0.0/Problems/${p:0:3}/$p.p" --github || true
done <./.github/thf_tests.txt
- name: Test TFF
run: |
while read p; do
echo "TFF Problem: $p"
timeout 30 ./build/bin/duper "../TPTP-v8.0.0/Problems/${p:0:3}/$p.p" --github || true
done <./.github/tff_tests.txt
- name: Test FOF
run: |
while read p; do
echo "FOF Problem: $p"
timeout 30 ./build/bin/duper "../TPTP-v8.0.0/Problems/${p:0:3}/$p.p" --github || true
done <./.github/fof_tests.txt