src/HOL/TPTP/lib/Tools/tptp_isabelle
author blanchet
Mon, 23 Jan 2012 17:40:31 +0100
changeset 46319 c248e4f1be74
child 46324 e4bccf5ec61e
permissions -rwxr-xr-x
rebranded Nitrox, for more uniformity
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
#
c248e4f1be74 rebranded Nitrox, for more uniformity
blanchet
parents:
diff changeset
     5
# DESCRIPTION: Isabelle tactics for TPTP
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
c248e4f1be74 rebranded Nitrox, for more uniformity
blanchet
parents:
diff changeset
    12
  echo "Usage: isabelle $PRG FILES"
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."
c248e4f1be74 rebranded Nitrox, for more uniformity
blanchet
parents:
diff changeset
    15
  echo
c248e4f1be74 rebranded Nitrox, for more uniformity
blanchet
parents:
diff changeset
    16
  exit 1
c248e4f1be74 rebranded Nitrox, for more uniformity
blanchet
parents:
diff changeset
    17
}
c248e4f1be74 rebranded Nitrox, for more uniformity
blanchet
parents:
diff changeset
    18
c248e4f1be74 rebranded Nitrox, for more uniformity
blanchet
parents:
diff changeset
    19
[ "$#" -eq 0 -o "$1" = "-?" ] && usage
c248e4f1be74 rebranded Nitrox, for more uniformity
blanchet
parents:
diff changeset
    20
c248e4f1be74 rebranded Nitrox, for more uniformity
blanchet
parents:
diff changeset
    21
SCRATCH="Scratch_${PRG}_$$_${RANDOM}"
c248e4f1be74 rebranded Nitrox, for more uniformity
blanchet
parents:
diff changeset
    22
c248e4f1be74 rebranded Nitrox, for more uniformity
blanchet
parents:
diff changeset
    23
for FILE in "$@"
c248e4f1be74 rebranded Nitrox, for more uniformity
blanchet
parents:
diff changeset
    24
do
c248e4f1be74 rebranded Nitrox, for more uniformity
blanchet
parents:
diff changeset
    25
  echo "theory $SCRATCH imports \"CASC\_Setup\" begin ML {* FIXME \"$FILE\" *} end;" \
c248e4f1be74 rebranded Nitrox, for more uniformity
blanchet
parents:
diff changeset
    26
    > /tmp/$SCRATCH.thy
c248e4f1be74 rebranded Nitrox, for more uniformity
blanchet
parents:
diff changeset
    27
  "$ISABELLE_PROCESS" -e "use_thy \"/tmp/$SCRATCH\"; exit 1;"
c248e4f1be74 rebranded Nitrox, for more uniformity
blanchet
parents:
diff changeset
    28
done