src/HOL/TPTP/lib/Tools/tptp_nitpick
author blanchet
Mon Jan 23 17:40:31 2012 +0100 (2012-01-23)
changeset 46319 c248e4f1be74
parent 46318 src/HOL/TPTP/lib/Tools/nitrox@8038d050ff15
child 46324 e4bccf5ec61e
permissions -rwxr-xr-x
rebranded Nitrox, for more uniformity
blanchet@42064
     1
#!/usr/bin/env bash
blanchet@42064
     2
#
blanchet@42064
     3
# Author: Jasmin Blanchette
blanchet@42064
     4
#
blanchet@46319
     5
# DESCRIPTION: Nitpick for TPTP
blanchet@42064
     6
blanchet@42064
     7
blanchet@42064
     8
PRG="$(basename "$0")"
blanchet@42064
     9
blanchet@42064
    10
function usage() {
blanchet@42064
    11
  echo
blanchet@42064
    12
  echo "Usage: isabelle $PRG FILES"
blanchet@42064
    13
  echo
blanchet@46319
    14
  echo "  Runs Nitpick on TPTP problems."
blanchet@42064
    15
  echo
blanchet@42064
    16
  exit 1
blanchet@42064
    17
}
blanchet@42064
    18
blanchet@42108
    19
[ "$#" -eq 0 -o "$1" = "-?" ] && usage
blanchet@42108
    20
blanchet@43811
    21
SCRATCH="Scratch_${PRG}_$$_${RANDOM}"
blanchet@43811
    22
blanchet@42064
    23
for FILE in "$@"
blanchet@42064
    24
do
blanchet@46319
    25
  echo "theory $SCRATCH imports \"Main\" begin ML {* Nitpick_TPTP.pick_nits_in_tptp_file \"$FILE\" *} end;" \
blanchet@43811
    26
    > /tmp/$SCRATCH.thy
wenzelm@43836
    27
  "$ISABELLE_PROCESS" -e "use_thy \"/tmp/$SCRATCH\"; exit 1;"
blanchet@42064
    28
done