Mercurial Mercurial > repos > isabelle / annotate
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/TPTP/lib/Tools/tptp_nitpick
author blanchet
Mon, 23 Jan 2012 17:40:32 +0100
changeset 46324 e4bccf5ec61e
parent 46319 c248e4f1be74
child 47670 24babc4b1925
permissions -rwxr-xr-x
added problem importer
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
42064
f4e53c8630c0 added first-order TPTP version of Nitpick to Isabelle, so that its sources stay in sync with Isabelle and it is easier to install new versions for SystemOnTPTP and CASC -- the tool is called "isabelle nitrox" but is deliberately omitted from the tool list unless the component is explicitly enabled, to avoid clutter
blanchet
parents:
diff changeset 
     1
 
#!/usr/bin/env bash
f4e53c8630c0 added first-order TPTP version of Nitpick to Isabelle, so that its sources stay in sync with Isabelle and it is easier to install new versions for SystemOnTPTP and CASC -- the tool is called "isabelle nitrox" but is deliberately omitted from the tool list unless the component is explicitly enabled, to avoid clutter
blanchet
parents:
diff changeset 
     2
 
#
f4e53c8630c0 added first-order TPTP version of Nitpick to Isabelle, so that its sources stay in sync with Isabelle and it is easier to install new versions for SystemOnTPTP and CASC -- the tool is called "isabelle nitrox" but is deliberately omitted from the tool list unless the component is explicitly enabled, to avoid clutter
blanchet
parents:
diff changeset 
     3
 
# Author: Jasmin Blanchette
f4e53c8630c0 added first-order TPTP version of Nitpick to Isabelle, so that its sources stay in sync with Isabelle and it is easier to install new versions for SystemOnTPTP and CASC -- the tool is called "isabelle nitrox" but is deliberately omitted from the tool list unless the component is explicitly enabled, to avoid clutter
blanchet
parents:
diff changeset 
     4
 
#
46319
c248e4f1be74 rebranded Nitrox, for more uniformity
blanchet
parents: 46318
diff changeset 
     5
 
# DESCRIPTION: Nitpick for TPTP
42064
f4e53c8630c0 added first-order TPTP version of Nitpick to Isabelle, so that its sources stay in sync with Isabelle and it is easier to install new versions for SystemOnTPTP and CASC -- the tool is called "isabelle nitrox" but is deliberately omitted from the tool list unless the component is explicitly enabled, to avoid clutter
blanchet
parents:
diff changeset 
     6
 












f4e53c8630c0
added first-order TPTP version of Nitpick to Isabelle, so that its sources stay in sync with Isabelle and it is easier to install new versions for SystemOnTPTP and CASC -- the tool is called "isabelle nitrox" but is deliberately omitted from the tool list unless the component is explicitly enabled, to avoid clutter



blanchet


parents: 

diff
changeset




     7














f4e53c8630c0
added first-order TPTP version of Nitpick to Isabelle, so that its sources stay in sync with Isabelle and it is easier to install new versions for SystemOnTPTP and CASC -- the tool is called "isabelle nitrox" but is deliberately omitted from the tool list unless the component is explicitly enabled, to avoid clutter



blanchet


parents: 

diff
changeset




     8


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













f4e53c8630c0
added first-order TPTP version of Nitpick to Isabelle, so that its sources stay in sync with Isabelle and it is easier to install new versions for SystemOnTPTP and CASC -- the tool is called "isabelle nitrox" but is deliberately omitted from the tool list unless the component is explicitly enabled, to avoid clutter



blanchet


parents: 

diff
changeset




     9














f4e53c8630c0
added first-order TPTP version of Nitpick to Isabelle, so that its sources stay in sync with Isabelle and it is easier to install new versions for SystemOnTPTP and CASC -- the tool is called "isabelle nitrox" but is deliberately omitted from the tool list unless the component is explicitly enabled, to avoid clutter



blanchet


parents: 

diff
changeset




    10


function usage() {













f4e53c8630c0
added first-order TPTP version of Nitpick to Isabelle, so that its sources stay in sync with Isabelle and it is easier to install new versions for SystemOnTPTP and CASC -- the tool is called "isabelle nitrox" but is deliberately omitted from the tool list unless the component is explicitly enabled, to avoid clutter



blanchet


parents: 

diff
changeset




    11


  echo













f4e53c8630c0
added first-order TPTP version of Nitpick to Isabelle, so that its sources stay in sync with Isabelle and it is easier to install new versions for SystemOnTPTP and CASC -- the tool is called "isabelle nitrox" but is deliberately omitted from the tool list unless the component is explicitly enabled, to avoid clutter



blanchet


parents: 

diff
changeset




    12


  echo "Usage: isabelle $PRG FILES"













f4e53c8630c0
added first-order TPTP version of Nitpick to Isabelle, so that its sources stay in sync with Isabelle and it is easier to install new versions for SystemOnTPTP and CASC -- the tool is called "isabelle nitrox" but is deliberately omitted from the tool list unless the component is explicitly enabled, to avoid clutter



blanchet


parents: 

diff
changeset




    13


  echo








46319






c248e4f1be74
rebranded Nitrox, for more uniformity



blanchet


parents: 
46318

diff
changeset




    14


  echo "  Runs Nitpick on TPTP problems."








42064






f4e53c8630c0
added first-order TPTP version of Nitpick to Isabelle, so that its sources stay in sync with Isabelle and it is easier to install new versions for SystemOnTPTP and CASC -- the tool is called "isabelle nitrox" but is deliberately omitted from the tool list unless the component is explicitly enabled, to avoid clutter



blanchet


parents: 

diff
changeset




    15


  echo













f4e53c8630c0
added first-order TPTP version of Nitpick to Isabelle, so that its sources stay in sync with Isabelle and it is easier to install new versions for SystemOnTPTP and CASC -- the tool is called "isabelle nitrox" but is deliberately omitted from the tool list unless the component is explicitly enabled, to avoid clutter



blanchet


parents: 

diff
changeset




    16


  exit 1













f4e53c8630c0
added first-order TPTP version of Nitpick to Isabelle, so that its sources stay in sync with Isabelle and it is easier to install new versions for SystemOnTPTP and CASC -- the tool is called "isabelle nitrox" but is deliberately omitted from the tool list unless the component is explicitly enabled, to avoid clutter



blanchet


parents: 

diff
changeset




    17


}













f4e53c8630c0
added first-order TPTP version of Nitpick to Isabelle, so that its sources stay in sync with Isabelle and it is easier to install new versions for SystemOnTPTP and CASC -- the tool is called "isabelle nitrox" but is deliberately omitted from the tool list unless the component is explicitly enabled, to avoid clutter



blanchet


parents: 

diff
changeset




    18









42108






f55562e77d5c
add "-?" to "nitrox" tool



blanchet


parents: 
42064

diff
changeset




    19


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













f55562e77d5c
add "-?" to "nitrox" tool



blanchet


parents: 
42064

diff
changeset




    20









43811






402e1a0d93d9
better temp name creation for Nitrox -- still very hackish though, but should get us through CASC-23 and CASC-J6



blanchet


parents: 
43808

diff
changeset




    21


SCRATCH="Scratch_${PRG}_$$_${RANDOM}"













402e1a0d93d9
better temp name creation for Nitrox -- still very hackish though, but should get us through CASC-23 and CASC-J6



blanchet


parents: 
43808

diff
changeset




    22









42064






f4e53c8630c0
added first-order TPTP version of Nitpick to Isabelle, so that its sources stay in sync with Isabelle and it is easier to install new versions for SystemOnTPTP and CASC -- the tool is called "isabelle nitrox" but is deliberately omitted from the tool list unless the component is explicitly enabled, to avoid clutter



blanchet


parents: 

diff
changeset




    23


for FILE in "$@"













f4e53c8630c0
added first-order TPTP version of Nitpick to Isabelle, so that its sources stay in sync with Isabelle and it is easier to install new versions for SystemOnTPTP and CASC -- the tool is called "isabelle nitrox" but is deliberately omitted from the tool list unless the component is explicitly enabled, to avoid clutter



blanchet


parents: 

diff
changeset




    24


do








46324






e4bccf5ec61e
added problem importer



blanchet


parents: 
46319

diff
changeset




    25


  echo "theory $SCRATCH imports \"$TPTP_HOME/ATP_Problem_Import\" begin \













e4bccf5ec61e
added problem importer



blanchet


parents: 
46319

diff
changeset




    26


ML {* ATP_Problem_Import.nitpick_tptp_file \"$FILE\" *} end;" \








43811






402e1a0d93d9
better temp name creation for Nitrox -- still very hackish though, but should get us through CASC-23 and CASC-J6



blanchet


parents: 
43808

diff
changeset




    27


    > /tmp/$SCRATCH.thy








43836






136ac1de4cbc
more quotes;



wenzelm


parents: 
43811

diff
changeset




    28


  "$ISABELLE_PROCESS" -e "use_thy \"/tmp/$SCRATCH\"; exit 1;"








42064






f4e53c8630c0
added first-order TPTP version of Nitpick to Isabelle, so that its sources stay in sync with Isabelle and it is easier to install new versions for SystemOnTPTP and CASC -- the tool is called "isabelle nitrox" but is deliberately omitted from the tool list unless the component is explicitly enabled, to avoid clutter



blanchet


parents: 

diff
changeset




    29


done















isabelle