equal
deleted
inserted
replaced
24 args=("$@") |
24 args=("$@") |
25 |
25 |
26 isabelle build -b HOL-TPTP 2>&1 | grep --line-buffered -v "elapsed time$" |
26 isabelle build -b HOL-TPTP 2>&1 | grep --line-buffered -v "elapsed time$" |
27 |
27 |
28 echo "theory $SCRATCH imports \"$TPTP_HOME/ATP_Problem_Import\" begin \ |
28 echo "theory $SCRATCH imports \"$TPTP_HOME/ATP_Problem_Import\" begin \ |
29 ML {* ATP_Problem_Import.translate_tptp_file @{theory} \"${args[0]}\" \"${args[1]}\" *} end" \ |
29 ML \<open> ATP_Problem_Import.translate_tptp_file @{theory} \"${args[0]}\" \"${args[1]}\" \<close> end" \ |
30 > /tmp/$SCRATCH.thy |
30 > /tmp/$SCRATCH.thy |
31 isabelle process -e "use_thy \"/tmp/$SCRATCH\"; exit 1;" -l HOL-TPTP | grep --line-buffered -v "^###\|^PROOF FAILED for depth\|^Failure node\|inferences so far. Searching to depth\|^val \|^Loading theory\|^poly.*warning: The type of\|^ monotype.$" |
31 isabelle process -e "use_thy \"/tmp/$SCRATCH\"; exit 1;" -l HOL-TPTP | grep --line-buffered -v "^###\|^PROOF FAILED for depth\|^Failure node\|inferences so far. Searching to depth\|^val \|^Loading theory\|^poly.*warning: The type of\|^ monotype.$" |