author | boehmes |
Fri, 21 Aug 2009 13:21:19 +0200 | |
changeset 32385 | 594890623c46 |
parent 32383 | 521065a499c6 |
child 32397 | 1899b8c47961 |
permissions | -rwxr-xr-x |
32382
98674ac811c4
Mirabelle tool script conforming to standard Isabelle tool interface,
boehmes
parents:
32381
diff
changeset
|
1 |
#!/usr/bin/env bash |
98674ac811c4
Mirabelle tool script conforming to standard Isabelle tool interface,
boehmes
parents:
32381
diff
changeset
|
2 |
# |
98674ac811c4
Mirabelle tool script conforming to standard Isabelle tool interface,
boehmes
parents:
32381
diff
changeset
|
3 |
# Author: Sascha Boehme |
98674ac811c4
Mirabelle tool script conforming to standard Isabelle tool interface,
boehmes
parents:
32381
diff
changeset
|
4 |
# |
98674ac811c4
Mirabelle tool script conforming to standard Isabelle tool interface,
boehmes
parents:
32381
diff
changeset
|
5 |
# DESCRIPTION: testing tool for automated proof tools |
32381 | 6 |
|
7 |
||
32382
98674ac811c4
Mirabelle tool script conforming to standard Isabelle tool interface,
boehmes
parents:
32381
diff
changeset
|
8 |
PRG="$(basename "$0")" |
32381 | 9 |
|
32385
594890623c46
split actions from Mirabelle core (Mirabelle may thus be applied to basic theories in HOL)
boehmes
parents:
32383
diff
changeset
|
10 |
function action_names() { |
594890623c46
split actions from Mirabelle core (Mirabelle may thus be applied to basic theories in HOL)
boehmes
parents:
32383
diff
changeset
|
11 |
TOOLS="$MIRABELLE_HOME/Tools/mirabelle_*.ML" |
594890623c46
split actions from Mirabelle core (Mirabelle may thus be applied to basic theories in HOL)
boehmes
parents:
32383
diff
changeset
|
12 |
ACTION_NAMES=`find $TOOLS | sed 's/.*mirabelle_\(.*\)\.ML/\1/'` |
594890623c46
split actions from Mirabelle core (Mirabelle may thus be applied to basic theories in HOL)
boehmes
parents:
32383
diff
changeset
|
13 |
} |
594890623c46
split actions from Mirabelle core (Mirabelle may thus be applied to basic theories in HOL)
boehmes
parents:
32383
diff
changeset
|
14 |
|
32382
98674ac811c4
Mirabelle tool script conforming to standard Isabelle tool interface,
boehmes
parents:
32381
diff
changeset
|
15 |
function usage() { |
98674ac811c4
Mirabelle tool script conforming to standard Isabelle tool interface,
boehmes
parents:
32381
diff
changeset
|
16 |
out="$MIRABELLE_OUTPUT_PATH" |
98674ac811c4
Mirabelle tool script conforming to standard Isabelle tool interface,
boehmes
parents:
32381
diff
changeset
|
17 |
timeout="$MIRABELLE_TIMEOUT" |
32385
594890623c46
split actions from Mirabelle core (Mirabelle may thus be applied to basic theories in HOL)
boehmes
parents:
32383
diff
changeset
|
18 |
action_names |
32382
98674ac811c4
Mirabelle tool script conforming to standard Isabelle tool interface,
boehmes
parents:
32381
diff
changeset
|
19 |
echo |
98674ac811c4
Mirabelle tool script conforming to standard Isabelle tool interface,
boehmes
parents:
32381
diff
changeset
|
20 |
echo "Usage: isabelle $PRG [OPTIONS] ACTIONS FILES" |
98674ac811c4
Mirabelle tool script conforming to standard Isabelle tool interface,
boehmes
parents:
32381
diff
changeset
|
21 |
echo |
98674ac811c4
Mirabelle tool script conforming to standard Isabelle tool interface,
boehmes
parents:
32381
diff
changeset
|
22 |
echo " Options are:" |
98674ac811c4
Mirabelle tool script conforming to standard Isabelle tool interface,
boehmes
parents:
32381
diff
changeset
|
23 |
echo " -L LOGIC parent logic to use (default $ISABELLE_LOGIC)" |
32385
594890623c46
split actions from Mirabelle core (Mirabelle may thus be applied to basic theories in HOL)
boehmes
parents:
32383
diff
changeset
|
24 |
echo " -T THEORY parent theory to use (default $MIRABELLE_THEORY)" |
32382
98674ac811c4
Mirabelle tool script conforming to standard Isabelle tool interface,
boehmes
parents:
32381
diff
changeset
|
25 |
echo " -O DIR output directory for test data (default $out)" |
98674ac811c4
Mirabelle tool script conforming to standard Isabelle tool interface,
boehmes
parents:
32381
diff
changeset
|
26 |
echo " -v be verbose" |
98674ac811c4
Mirabelle tool script conforming to standard Isabelle tool interface,
boehmes
parents:
32381
diff
changeset
|
27 |
echo " -t TIMEOUT timeout for each action in seconds (default $timeout)" |
98674ac811c4
Mirabelle tool script conforming to standard Isabelle tool interface,
boehmes
parents:
32381
diff
changeset
|
28 |
echo |
98674ac811c4
Mirabelle tool script conforming to standard Isabelle tool interface,
boehmes
parents:
32381
diff
changeset
|
29 |
echo " Apply the given actions (i.e., automated proof tools)" |
98674ac811c4
Mirabelle tool script conforming to standard Isabelle tool interface,
boehmes
parents:
32381
diff
changeset
|
30 |
echo " at all proof steps in the given theory files." |
98674ac811c4
Mirabelle tool script conforming to standard Isabelle tool interface,
boehmes
parents:
32381
diff
changeset
|
31 |
echo |
98674ac811c4
Mirabelle tool script conforming to standard Isabelle tool interface,
boehmes
parents:
32381
diff
changeset
|
32 |
echo " ACTIONS is a colon-separated list of actions, where each action is" |
32385
594890623c46
split actions from Mirabelle core (Mirabelle may thus be applied to basic theories in HOL)
boehmes
parents:
32383
diff
changeset
|
33 |
echo " either NAME or NAME[KEY=VALUE,...,KEY=VALUE]. Available actions are:" |
594890623c46
split actions from Mirabelle core (Mirabelle may thus be applied to basic theories in HOL)
boehmes
parents:
32383
diff
changeset
|
34 |
for NAME in $ACTION_NAMES |
594890623c46
split actions from Mirabelle core (Mirabelle may thus be applied to basic theories in HOL)
boehmes
parents:
32383
diff
changeset
|
35 |
do |
594890623c46
split actions from Mirabelle core (Mirabelle may thus be applied to basic theories in HOL)
boehmes
parents:
32383
diff
changeset
|
36 |
echo " $NAME" |
594890623c46
split actions from Mirabelle core (Mirabelle may thus be applied to basic theories in HOL)
boehmes
parents:
32383
diff
changeset
|
37 |
done |
32382
98674ac811c4
Mirabelle tool script conforming to standard Isabelle tool interface,
boehmes
parents:
32381
diff
changeset
|
38 |
echo |
98674ac811c4
Mirabelle tool script conforming to standard Isabelle tool interface,
boehmes
parents:
32381
diff
changeset
|
39 |
echo " FILES is a space-separated list of theory files, where each file is" |
98674ac811c4
Mirabelle tool script conforming to standard Isabelle tool interface,
boehmes
parents:
32381
diff
changeset
|
40 |
echo " either NAME.thy or NAME.thy[START:END] and START and END are numbers" |
98674ac811c4
Mirabelle tool script conforming to standard Isabelle tool interface,
boehmes
parents:
32381
diff
changeset
|
41 |
echo " indicating the range the given actions are to be applied." |
98674ac811c4
Mirabelle tool script conforming to standard Isabelle tool interface,
boehmes
parents:
32381
diff
changeset
|
42 |
echo |
98674ac811c4
Mirabelle tool script conforming to standard Isabelle tool interface,
boehmes
parents:
32381
diff
changeset
|
43 |
exit 1 |
32381 | 44 |
} |
45 |
||
46 |
||
32382
98674ac811c4
Mirabelle tool script conforming to standard Isabelle tool interface,
boehmes
parents:
32381
diff
changeset
|
47 |
## process command line |
32381 | 48 |
|
32382
98674ac811c4
Mirabelle tool script conforming to standard Isabelle tool interface,
boehmes
parents:
32381
diff
changeset
|
49 |
# options |
32381 | 50 |
|
32385
594890623c46
split actions from Mirabelle core (Mirabelle may thus be applied to basic theories in HOL)
boehmes
parents:
32383
diff
changeset
|
51 |
while getopts "L:T:O:vt:" OPT |
32382
98674ac811c4
Mirabelle tool script conforming to standard Isabelle tool interface,
boehmes
parents:
32381
diff
changeset
|
52 |
do |
98674ac811c4
Mirabelle tool script conforming to standard Isabelle tool interface,
boehmes
parents:
32381
diff
changeset
|
53 |
case "$OPT" in |
98674ac811c4
Mirabelle tool script conforming to standard Isabelle tool interface,
boehmes
parents:
32381
diff
changeset
|
54 |
L) |
98674ac811c4
Mirabelle tool script conforming to standard Isabelle tool interface,
boehmes
parents:
32381
diff
changeset
|
55 |
MIRABELLE_LOGIC="$OPTARG" |
98674ac811c4
Mirabelle tool script conforming to standard Isabelle tool interface,
boehmes
parents:
32381
diff
changeset
|
56 |
;; |
32385
594890623c46
split actions from Mirabelle core (Mirabelle may thus be applied to basic theories in HOL)
boehmes
parents:
32383
diff
changeset
|
57 |
T) |
594890623c46
split actions from Mirabelle core (Mirabelle may thus be applied to basic theories in HOL)
boehmes
parents:
32383
diff
changeset
|
58 |
MIRABELLE_THEORY="$OPTARG" |
594890623c46
split actions from Mirabelle core (Mirabelle may thus be applied to basic theories in HOL)
boehmes
parents:
32383
diff
changeset
|
59 |
;; |
32382
98674ac811c4
Mirabelle tool script conforming to standard Isabelle tool interface,
boehmes
parents:
32381
diff
changeset
|
60 |
O) |
98674ac811c4
Mirabelle tool script conforming to standard Isabelle tool interface,
boehmes
parents:
32381
diff
changeset
|
61 |
MIRABELLE_OUTPUT_PATH="$OPTARG" |
98674ac811c4
Mirabelle tool script conforming to standard Isabelle tool interface,
boehmes
parents:
32381
diff
changeset
|
62 |
;; |
98674ac811c4
Mirabelle tool script conforming to standard Isabelle tool interface,
boehmes
parents:
32381
diff
changeset
|
63 |
v) |
98674ac811c4
Mirabelle tool script conforming to standard Isabelle tool interface,
boehmes
parents:
32381
diff
changeset
|
64 |
MIRABELLE_VERBOSE=true |
98674ac811c4
Mirabelle tool script conforming to standard Isabelle tool interface,
boehmes
parents:
32381
diff
changeset
|
65 |
;; |
98674ac811c4
Mirabelle tool script conforming to standard Isabelle tool interface,
boehmes
parents:
32381
diff
changeset
|
66 |
t) |
98674ac811c4
Mirabelle tool script conforming to standard Isabelle tool interface,
boehmes
parents:
32381
diff
changeset
|
67 |
MIRABELLE_TIMEOUT="$OPTARG" |
98674ac811c4
Mirabelle tool script conforming to standard Isabelle tool interface,
boehmes
parents:
32381
diff
changeset
|
68 |
;; |
98674ac811c4
Mirabelle tool script conforming to standard Isabelle tool interface,
boehmes
parents:
32381
diff
changeset
|
69 |
\?) |
98674ac811c4
Mirabelle tool script conforming to standard Isabelle tool interface,
boehmes
parents:
32381
diff
changeset
|
70 |
usage |
98674ac811c4
Mirabelle tool script conforming to standard Isabelle tool interface,
boehmes
parents:
32381
diff
changeset
|
71 |
;; |
98674ac811c4
Mirabelle tool script conforming to standard Isabelle tool interface,
boehmes
parents:
32381
diff
changeset
|
72 |
esac |
98674ac811c4
Mirabelle tool script conforming to standard Isabelle tool interface,
boehmes
parents:
32381
diff
changeset
|
73 |
done |
32381 | 74 |
|
32382
98674ac811c4
Mirabelle tool script conforming to standard Isabelle tool interface,
boehmes
parents:
32381
diff
changeset
|
75 |
shift $(($OPTIND - 1)) |
98674ac811c4
Mirabelle tool script conforming to standard Isabelle tool interface,
boehmes
parents:
32381
diff
changeset
|
76 |
|
98674ac811c4
Mirabelle tool script conforming to standard Isabelle tool interface,
boehmes
parents:
32381
diff
changeset
|
77 |
ACTIONS="$1" |
32381 | 78 |
|
32382
98674ac811c4
Mirabelle tool script conforming to standard Isabelle tool interface,
boehmes
parents:
32381
diff
changeset
|
79 |
shift |
32381 | 80 |
|
32382
98674ac811c4
Mirabelle tool script conforming to standard Isabelle tool interface,
boehmes
parents:
32381
diff
changeset
|
81 |
|
98674ac811c4
Mirabelle tool script conforming to standard Isabelle tool interface,
boehmes
parents:
32381
diff
changeset
|
82 |
# setup |
32381 | 83 |
|
32382
98674ac811c4
Mirabelle tool script conforming to standard Isabelle tool interface,
boehmes
parents:
32381
diff
changeset
|
84 |
mkdir -p $MIRABELLE_OUTPUT_PATH |
98674ac811c4
Mirabelle tool script conforming to standard Isabelle tool interface,
boehmes
parents:
32381
diff
changeset
|
85 |
|
98674ac811c4
Mirabelle tool script conforming to standard Isabelle tool interface,
boehmes
parents:
32381
diff
changeset
|
86 |
|
98674ac811c4
Mirabelle tool script conforming to standard Isabelle tool interface,
boehmes
parents:
32381
diff
changeset
|
87 |
## main |
32381 | 88 |
|
32382
98674ac811c4
Mirabelle tool script conforming to standard Isabelle tool interface,
boehmes
parents:
32381
diff
changeset
|
89 |
for FILE in "$@" |
98674ac811c4
Mirabelle tool script conforming to standard Isabelle tool interface,
boehmes
parents:
32381
diff
changeset
|
90 |
do |
98674ac811c4
Mirabelle tool script conforming to standard Isabelle tool interface,
boehmes
parents:
32381
diff
changeset
|
91 |
perl -w $MIRABELLE_HOME/lib/scripts/mirabelle.pl $ACTIONS "$FILE" |
98674ac811c4
Mirabelle tool script conforming to standard Isabelle tool interface,
boehmes
parents:
32381
diff
changeset
|
92 |
done |
32381 | 93 |