moved "nitrox" to TPTP
authorblanchet
Mon Jan 23 17:40:31 2012 +0100 (2012-01-23)
changeset 463188038d050ff15
parent 46317 80dccedd6c14
child 46319 c248e4f1be74
moved "nitrox" to TPTP
etc/components
src/HOL/TPTP/etc/settings
src/HOL/TPTP/lib/Tools/nitrox
src/HOL/Tools/Nitpick/etc/settings
src/HOL/Tools/Nitpick/lib/Tools/nitrox
     1.1 --- a/etc/components	Mon Jan 23 17:29:19 2012 +0100
     1.2 +++ b/etc/components	Mon Jan 23 17:40:31 2012 +0100
     1.3 @@ -13,10 +13,10 @@
     1.4  src/Tools/Code
     1.5  src/Tools/jEdit
     1.6  src/Tools/WWW_Find
     1.7 +src/HOL/Mirabelle
     1.8 +src/HOL/Mutabelle
     1.9 +src/HOL/Library/Sum_of_Squares
    1.10  src/HOL/Tools/ATP
    1.11 -src/HOL/Mirabelle
    1.12 -src/HOL/Library/Sum_of_Squares
    1.13 +src/HOL/Tools/Predicate_Compile
    1.14  src/HOL/Tools/SMT
    1.15 -src/HOL/Tools/Predicate_Compile
    1.16 -src/HOL/Tools/Nitpick
    1.17 -src/HOL/Mutabelle
    1.18 +src/HOL/TPTP
     2.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.2 +++ b/src/HOL/TPTP/etc/settings	Mon Jan 23 17:40:31 2012 +0100
     2.3 @@ -0,0 +1,3 @@
     2.4 +# -*- shell-script -*- :mode=shellscript:
     2.5 +
     2.6 +ISABELLE_TOOLS="$ISABELLE_TOOLS:$COMPONENT/lib/Tools"
     3.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.2 +++ b/src/HOL/TPTP/lib/Tools/nitrox	Mon Jan 23 17:40:31 2012 +0100
     3.3 @@ -0,0 +1,28 @@
     3.4 +#!/usr/bin/env bash
     3.5 +#
     3.6 +# Author: Jasmin Blanchette
     3.7 +#
     3.8 +# DESCRIPTION: TPTP FOF version of Nitpick
     3.9 +
    3.10 +
    3.11 +PRG="$(basename "$0")"
    3.12 +
    3.13 +function usage() {
    3.14 +  echo
    3.15 +  echo "Usage: isabelle $PRG FILES"
    3.16 +  echo
    3.17 +  echo "  Runs Nitrox on a CNF or FOF TPTP problem."
    3.18 +  echo
    3.19 +  exit 1
    3.20 +}
    3.21 +
    3.22 +[ "$#" -eq 0 -o "$1" = "-?" ] && usage
    3.23 +
    3.24 +SCRATCH="Scratch_${PRG}_$$_${RANDOM}"
    3.25 +
    3.26 +for FILE in "$@"
    3.27 +do
    3.28 +  echo "theory $SCRATCH imports \"Nitpick\" begin ML {* Nitrox.pick_nits_in_fof_file \"$FILE\" *} end;" \
    3.29 +    > /tmp/$SCRATCH.thy
    3.30 +  "$ISABELLE_PROCESS" -e "use_thy \"/tmp/$SCRATCH\"; exit 1;"
    3.31 +done
     4.1 --- a/src/HOL/Tools/Nitpick/etc/settings	Mon Jan 23 17:29:19 2012 +0100
     4.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     4.3 @@ -1,3 +0,0 @@
     4.4 -# -*- shell-script -*- :mode=shellscript:
     4.5 -
     4.6 -ISABELLE_TOOLS="$ISABELLE_TOOLS:$COMPONENT/lib/Tools"
     5.1 --- a/src/HOL/Tools/Nitpick/lib/Tools/nitrox	Mon Jan 23 17:29:19 2012 +0100
     5.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     5.3 @@ -1,28 +0,0 @@
     5.4 -#!/usr/bin/env bash
     5.5 -#
     5.6 -# Author: Jasmin Blanchette
     5.7 -#
     5.8 -# DESCRIPTION: TPTP FOF version of Nitpick
     5.9 -
    5.10 -
    5.11 -PRG="$(basename "$0")"
    5.12 -
    5.13 -function usage() {
    5.14 -  echo
    5.15 -  echo "Usage: isabelle $PRG FILES"
    5.16 -  echo
    5.17 -  echo "  Runs Nitrox on a FOF or CNF TPTP problem."
    5.18 -  echo
    5.19 -  exit 1
    5.20 -}
    5.21 -
    5.22 -[ "$#" -eq 0 -o "$1" = "-?" ] && usage
    5.23 -
    5.24 -SCRATCH="Scratch_${PRG}_$$_${RANDOM}"
    5.25 -
    5.26 -for FILE in "$@"
    5.27 -do
    5.28 -  echo "theory $SCRATCH imports \"Nitpick\" begin ML {* Nitrox.pick_nits_in_fof_file \"$FILE\" *} end;" \
    5.29 -    > /tmp/$SCRATCH.thy
    5.30 -  "$ISABELLE_PROCESS" -e "use_thy \"/tmp/$SCRATCH\"; exit 1;"
    5.31 -done