| author | blanchet |
| Wed, 13 Jul 2011 22:16:19 +0200 | |
| changeset 43808 | 8ba759b8caa8 |
| parent 42108 | f55562e77d5c |
| child 43811 | 402e1a0d93d9 |
| permissions | -rwxr-xr-x |
|
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 |
# |
|
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
|
5 |
# DESCRIPTION: TPTP FOF version of Nitpick |
|
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 |
|
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
|
14 |
echo " Runs Nitrox on a FOF or CNF TPTP problem." |
|
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 | 19 |
[ "$#" -eq 0 -o "$1" = "-?" ] && usage |
20 |
||
|
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
|
21 |
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
|
22 |
do |
|
43808
8ba759b8caa8
avoid relying on piping to "isabelle tty", because this gives errors on some Linuxes about the standard input not being a tty
blanchet
parents:
42108
diff
changeset
|
23 |
echo "theory Scratch imports \"Nitpick\" begin ML {* Nitrox.pick_nits_in_fof_file \"$FILE\" *} end;" \
|
|
8ba759b8caa8
avoid relying on piping to "isabelle tty", because this gives errors on some Linuxes about the standard input not being a tty
blanchet
parents:
42108
diff
changeset
|
24 |
> /tmp/$ISABELLE_TMP/Scratch.thy |
|
8ba759b8caa8
avoid relying on piping to "isabelle tty", because this gives errors on some Linuxes about the standard input not being a tty
blanchet
parents:
42108
diff
changeset
|
25 |
$ISABELLE_PROCESS -e "use_thy \"/tmp/$ISABELLE_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
|
26 |
done |