src/HOL/TPTP/lib/Tools/nitrox
changeset 46318 8038d050ff15
parent 43836 136ac1de4cbc
equal deleted inserted replaced
46317:80dccedd6c14 46318:8038d050ff15
       
     1 #!/usr/bin/env bash
       
     2 #
       
     3 # Author: Jasmin Blanchette
       
     4 #
       
     5 # DESCRIPTION: TPTP FOF version of Nitpick
       
     6 
       
     7 
       
     8 PRG="$(basename "$0")"
       
     9 
       
    10 function usage() {
       
    11   echo
       
    12   echo "Usage: isabelle $PRG FILES"
       
    13   echo
       
    14   echo "  Runs Nitrox on a CNF or FOF TPTP problem."
       
    15   echo
       
    16   exit 1
       
    17 }
       
    18 
       
    19 [ "$#" -eq 0 -o "$1" = "-?" ] && usage
       
    20 
       
    21 SCRATCH="Scratch_${PRG}_$$_${RANDOM}"
       
    22 
       
    23 for FILE in "$@"
       
    24 do
       
    25   echo "theory $SCRATCH imports \"Nitpick\" begin ML {* Nitrox.pick_nits_in_fof_file \"$FILE\" *} end;" \
       
    26     > /tmp/$SCRATCH.thy
       
    27   "$ISABELLE_PROCESS" -e "use_thy \"/tmp/$SCRATCH\"; exit 1;"
       
    28 done