# HG changeset patch
# User desharna
# Date 1761663873 -3600
# Node ID 19e7c4cece26fab8db8f0b8e4e8f0ba9c876f9a7
# Parent  7fca4140d4322d15cb06219175d4ef9eccf31d4e
adapted tptp_isabelle_hot to use new process_theory command

diff -r 7fca4140d432 -r 19e7c4cece26 src/HOL/TPTP/lib/Tools/tptp_isabelle_hot
--- a/src/HOL/TPTP/lib/Tools/tptp_isabelle_hot	Tue Oct 28 16:03:31 2025 +0100
+++ b/src/HOL/TPTP/lib/Tools/tptp_isabelle_hot	Tue Oct 28 16:04:33 2025 +0100
@@ -1,10 +1,10 @@
 #!/usr/bin/env bash
 #
 # Author: Jasmin Blanchette
+# Author: Martin Desharnais-Schäfer
 #
 # DESCRIPTION: Isabelle tactics for TPTP demo division
 
-
 PRG="$(basename "$0")"
 
 function usage() {
@@ -20,16 +20,29 @@
 [ "$#" -eq 0 -o "$1" = "-?" ] && usage
 
 SCRATCH="Scratch_${PRG}_$$_${RANDOM}"
+SCRATCH_FILE=/tmp/${SCRATCH}.thy
 
 TIMEOUT=$1
 shift
 
-isabelle build -b HOL-TPTP 2>&1 | grep --line-buffered -v "elapsed time$"
-
 for FILE in "$@"
 do
-  echo "theory $SCRATCH imports \"$TPTP_HOME/ATP_Problem_Import\" begin \
-ML {* ATP_Problem_Import.isabelle_hot_tptp_file @{theory} ($TIMEOUT) \"$FILE\" *} end" \
-    > /tmp/$SCRATCH.thy
-  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.$"
+  echo "theory ${SCRATCH} imports \"HOL-TPTP.ATP_Problem_Import\" begin \
+ML \<open> ATP_Problem_Import.isabelle_hot_tptp_file @{theory} (${TIMEOUT}) \"${FILE}\" \<close> end" \
+    > "${SCRATCH_FILE}"
+
+  isabelle process_theories -O -U -l HOL-TPTP -f "${SCRATCH_FILE}" "${SCRATCH}" \
+      | grep --line-buffered -vE \
+          -e '^Running Draft ...$' \
+          -e '^[[:space:]]*$' \
+          -e '^Output \(line [[:digit:]]+ of ".*"):$' \
+          -e '^val it = \(\): unit$' \
+          -e '^Finished Draft \([0-9:]+ elapsed time(, [0-9:]+ cpu time, factor [0-9.]+)?\)$' \
+          -e '^PROOF FAILED for depth' \
+          -e '^Failure node' \
+          -e 'inferences so far.  Searching to depth' \
+          -e '^val ' \
+          -e 'Loading theory' \
+          -e '^poly.*warning: The type of' \
+          -e '^   monotype.$'
 done