src/HOL/TPTP/lib/Tools/tptp_isabelle_hot
author immler
Tue, 10 Jul 2018 09:38:35 +0200 (2018-07-10)
changeset 68607 67bb59e49834
parent 64561 a7664ca9ffc5
permissions -rwxr-xr-x
make theorem, corollary, and proposition %important for HOL-Analysis manual
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
46319
c248e4f1be74 rebranded Nitrox, for more uniformity
blanchet
parents:
diff changeset
     1
#!/usr/bin/env bash
c248e4f1be74 rebranded Nitrox, for more uniformity
blanchet
parents:
diff changeset
     2
#
c248e4f1be74 rebranded Nitrox, for more uniformity
blanchet
parents:
diff changeset
     3
# Author: Jasmin Blanchette
c248e4f1be74 rebranded Nitrox, for more uniformity
blanchet
parents:
diff changeset
     4
#
47832
7df66b448c4a split into demo and competitive version
blanchet
parents: 47794
diff changeset
     5
# DESCRIPTION: Isabelle tactics for TPTP demo division
46319
c248e4f1be74 rebranded Nitrox, for more uniformity
blanchet
parents:
diff changeset
     6
c248e4f1be74 rebranded Nitrox, for more uniformity
blanchet
parents:
diff changeset
     7
c248e4f1be74 rebranded Nitrox, for more uniformity
blanchet
parents:
diff changeset
     8
PRG="$(basename "$0")"
c248e4f1be74 rebranded Nitrox, for more uniformity
blanchet
parents:
diff changeset
     9
c248e4f1be74 rebranded Nitrox, for more uniformity
blanchet
parents:
diff changeset
    10
function usage() {
c248e4f1be74 rebranded Nitrox, for more uniformity
blanchet
parents:
diff changeset
    11
  echo
47670
24babc4b1925 added timeout argument to TPTP tools
blanchet
parents: 46324
diff changeset
    12
  echo "Usage: isabelle $PRG TIMEOUT FILES"
46319
c248e4f1be74 rebranded Nitrox, for more uniformity
blanchet
parents:
diff changeset
    13
  echo
c248e4f1be74 rebranded Nitrox, for more uniformity
blanchet
parents:
diff changeset
    14
  echo "  Runs a combination of Isabelle tactics on TPTP problems."
47670
24babc4b1925 added timeout argument to TPTP tools
blanchet
parents: 46324
diff changeset
    15
  echo "  Each problem is allocated at most TIMEOUT seconds."
46319
c248e4f1be74 rebranded Nitrox, for more uniformity
blanchet
parents:
diff changeset
    16
  echo
c248e4f1be74 rebranded Nitrox, for more uniformity
blanchet
parents:
diff changeset
    17
  exit 1
c248e4f1be74 rebranded Nitrox, for more uniformity
blanchet
parents:
diff changeset
    18
}
c248e4f1be74 rebranded Nitrox, for more uniformity
blanchet
parents:
diff changeset
    19
c248e4f1be74 rebranded Nitrox, for more uniformity
blanchet
parents:
diff changeset
    20
[ "$#" -eq 0 -o "$1" = "-?" ] && usage
c248e4f1be74 rebranded Nitrox, for more uniformity
blanchet
parents:
diff changeset
    21
c248e4f1be74 rebranded Nitrox, for more uniformity
blanchet
parents:
diff changeset
    22
SCRATCH="Scratch_${PRG}_$$_${RANDOM}"
c248e4f1be74 rebranded Nitrox, for more uniformity
blanchet
parents:
diff changeset
    23
47670
24babc4b1925 added timeout argument to TPTP tools
blanchet
parents: 46324
diff changeset
    24
TIMEOUT=$1
24babc4b1925 added timeout argument to TPTP tools
blanchet
parents: 46324
diff changeset
    25
shift
24babc4b1925 added timeout argument to TPTP tools
blanchet
parents: 46324
diff changeset
    26
64561
a7664ca9ffc5 updated CASC instructions + tuning
blanchet
parents: 62634
diff changeset
    27
isabelle build -b HOL-TPTP 2>&1 | grep --line-buffered -v "elapsed time$"
60546
dcb0b9b42fcb automatically build image
blanchet
parents: 60545
diff changeset
    28
46319
c248e4f1be74 rebranded Nitrox, for more uniformity
blanchet
parents:
diff changeset
    29
for FILE in "$@"
c248e4f1be74 rebranded Nitrox, for more uniformity
blanchet
parents:
diff changeset
    30
do
46324
e4bccf5ec61e added problem importer
blanchet
parents: 46319
diff changeset
    31
  echo "theory $SCRATCH imports \"$TPTP_HOME/ATP_Problem_Import\" begin \
60544
3daf5eacec05 removed (now illegal) semicolons in generated theory files
blanchet
parents: 54434
diff changeset
    32
ML {* ATP_Problem_Import.isabelle_hot_tptp_file @{theory} ($TIMEOUT) \"$FILE\" *} end" \
46319
c248e4f1be74 rebranded Nitrox, for more uniformity
blanchet
parents:
diff changeset
    33
    > /tmp/$SCRATCH.thy
64561
a7664ca9ffc5 updated CASC instructions + tuning
blanchet
parents: 62634
diff changeset
    34
  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.$"
46319
c248e4f1be74 rebranded Nitrox, for more uniformity
blanchet
parents:
diff changeset
    35
done