equal
deleted
inserted
replaced
9 |
9 |
10 function usage() { |
10 function usage() { |
11 echo |
11 echo |
12 echo "Usage: isabelle $PRG FORMAT IN_FILE OUT_FILE" |
12 echo "Usage: isabelle $PRG FORMAT IN_FILE OUT_FILE" |
13 echo |
13 echo |
14 echo " Translates TPTP input file to specified TPTP format (\"FOF\", \"TFF0\", \"TFF1\", or \"THF0\")." |
14 echo " Translates TPTP input file to the specified format (\"FOF\", \"TFF0\", \"THF0\", or \"DFG\")." |
15 echo |
15 echo |
16 exit 1 |
16 exit 1 |
17 } |
17 } |
18 |
18 |
19 [ "$#" -ne 3 -o "$1" = "-?" ] && usage |
19 [ "$#" -ne 3 -o "$1" = "-?" ] && usage |
21 SCRATCH="Scratch_${PRG}_$$_${RANDOM}" |
21 SCRATCH="Scratch_${PRG}_$$_${RANDOM}" |
22 |
22 |
23 args=("$@") |
23 args=("$@") |
24 |
24 |
25 echo "theory $SCRATCH imports \"$TPTP_HOME/ATP_Problem_Import\" begin \ |
25 echo "theory $SCRATCH imports \"$TPTP_HOME/ATP_Problem_Import\" begin \ |
26 ML {* ATP_Problem_Import.translate_tptp_file \"${args[0]}\" \"${args[1]}\" \"${args[2]}\" *} end;" \ |
26 ML {* ATP_Problem_Import.translate_tptp_file @{theory} \"${args[0]}\" \"${args[1]}\" \"${args[2]}\" *} end;" \ |
27 > /tmp/$SCRATCH.thy |
27 > /tmp/$SCRATCH.thy |
28 "$ISABELLE_PROCESS" -q -e "use_thy \"/tmp/$SCRATCH\"; exit 1;" HOL-TPTP | grep --line-buffered -v "^###\|^PROOF FAILED for depth\|^Failure node\|inferences so far. Searching to depth\|^val it = (): unit" |
28 "$ISABELLE_PROCESS" -q -e "use_thy \"/tmp/$SCRATCH\"; exit 1;" HOL-TPTP | grep --line-buffered -v "^###\|^PROOF FAILED for depth\|^Failure node\|inferences so far. Searching to depth\|^val \|^Loading theory" |