Quelle  tptp_isabelle   Sprache: Text

#!/usr/bin/env bash
#
# Author: Jasmin Blanchette
# Author: Martin Desharnais-Schäfer
#
# DESCRIPTION: Isabelle tactics for TPTP competitive division

PRG="$(basename "$0")"

function usage() {
  echo
  echo "Usage: isabelle $PRG TIMEOUT FILES"
  echo
  echo "  Runs a combination of Isabelle tactics on TPTP problems."
  echo "  Each problem is allocated at most TIMEOUT seconds."
  echo
  exit 1
}

[ "$#" -eq 0 -o "$1" = "-?" ] && usage

SCRATCH="Scratch_${PRG}_$$_${RANDOM}"
SCRATCH_FILE=/tmp/${SCRATCH}.thy

TIMEOUT=$1
shift

for FILE in "$@"
do
  echo "theory ${SCRATCH} imports \"HOL-TPTP.ATP_Problem_Import\" begin \
ML \<open> ATP_Problem_Import.isabelle_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