equal
deleted
inserted
replaced
|
1 #!/usr/bin/env bash |
|
2 # |
|
3 # Author: Jasmin Blanchette |
|
4 # |
|
5 # DESCRIPTION: Isabelle tactics for TPTP competitive division |
|
6 |
|
7 |
|
8 PRG="$(basename "$0")" |
|
9 |
|
10 function usage() { |
|
11 echo |
|
12 echo "Usage: isabelle $PRG TIMEOUT FILES" |
|
13 echo |
|
14 echo " Runs a combination of Isabelle tactics on TPTP problems." |
|
15 echo " Each problem is allocated at most TIMEOUT seconds." |
|
16 echo |
|
17 exit 1 |
|
18 } |
|
19 |
|
20 [ "$#" -eq 0 -o "$1" = "-?" ] && usage |
|
21 |
|
22 SCRATCH="Scratch_${PRG}_$$_${RANDOM}" |
|
23 |
|
24 TIMEOUT=$1 |
|
25 shift |
|
26 |
|
27 for FILE in "$@" |
|
28 do |
|
29 echo "theory $SCRATCH imports \"$TPTP_HOME/ATP_Problem_Import\" begin \ |
|
30 ML {* ATP_Problem_Import.isabelle_comp_tptp_file @{theory} ($TIMEOUT) \"$FILE\" *} end;" \ |
|
31 > /tmp/$SCRATCH.thy |
|
32 "$ISABELLE_PROCESS" -e "use_thy \"/tmp/$SCRATCH\"; exit 1;" |
|
33 done |