| author | blanchet |
| Thu, 24 Mar 2011 17:56:59 +0100 | |
| changeset 42108 | f55562e77d5c |
| parent 42064 | f4e53c8630c0 |
| child 43808 | 8ba759b8caa8 |
| 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 |
|
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 |
(echo "theory Nitrox_Run imports Main begin" && |
|
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 |
echo "ML {* Nitrox.pick_nits_in_fof_file \"$FILE\" *}" &&
|
|
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
|
25 |
echo "end;") | isabelle tty |
|
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 |