Skip to content

Update lean-auto

Update lean-auto #552

Workflow file for this run

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