| author | blanchet |
| Mon, 23 Jan 2012 17:40:31 +0100 | |
| changeset 46318 | 8038d050ff15 |
| parent 43836 | src/HOL/Tools/Nitpick/lib/Tools/nitrox@136ac1de4cbc |
| 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 |
| 46318 | 14 |
echo " Runs Nitrox on a CNF or FOF TPTP problem." |
|
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 | 19 |
[ "$#" -eq 0 -o "$1" = "-?" ] && usage |
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 |
|
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
|
25 |
echo "theory $SCRATCH imports \"Nitpick\" begin ML {* Nitrox.pick_nits_in_fof_file \"$FILE\" *} end;" \
|
|
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
|
26 |
> /tmp/$SCRATCH.thy |
| 43836 | 27 |
"$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
|
28 |
done |