author | paulson |
Tue, 13 Jul 1999 10:42:31 +0200 | |
changeset 6988 | eed63543a3af |
parent 6256 | e17fb80b3ce1 |
child 7277 | bb9502f9154a |
permissions | -rwxr-xr-x |
3255 | 1 |
#!/bin/bash |
2755 | 2 |
# |
3 |
# $Id$ |
|
4 |
# |
|
2902 | 5 |
# build - compile the Isabelle system and object-logics |
2755 | 6 |
|
7 |
||
4457 | 8 |
## global settings |
9 |
||
10 |
ALL_LOGICS="CCL CTT Cube FOL FOLP HOL HOLCF LCF Pure Sequents ZF" |
|
11 |
||
12 |
||
2789 | 13 |
## settings |
14 |
||
15 |
PRG=$(basename $0) |
|
2755 | 16 |
|
2789 | 17 |
ISABELLE_HOME=$(dirname $0) |
18 |
. $ISABELLE_HOME/lib/scripts/getsettings || \ |
|
2936
bd33e7aae062
fixed { ... } shell syntax to accomodate bash 2.x;
wenzelm
parents:
2918
diff
changeset
|
19 |
{ echo "$PRG probably not called from its original place!"; exit 2; } |
2755 | 20 |
|
2789 | 21 |
|
2879 | 22 |
## diagnostics |
23 |
||
24 |
function usage() |
|
25 |
{ |
|
26 |
echo |
|
27 |
echo "Usage: $PRG [OPTIONS] [LOGICS ...]" |
|
28 |
echo |
|
29 |
echo " Options are:" |
|
30 |
echo " -a all logics" |
|
2902 | 31 |
echo " -b batch mode" |
6256 | 32 |
echo " -i make images" |
33 |
echo " -t make test" |
|
2879 | 34 |
echo |
3184 | 35 |
echo " Compile the named LOGICS (default $ISABELLE_LOGIC), or all object logics" |
2879 | 36 |
echo " in the distribution." |
37 |
echo |
|
38 |
exit 1 |
|
39 |
} |
|
40 |
||
41 |
function fail() |
|
42 |
{ |
|
43 |
echo "$1" >&2 |
|
44 |
exit 2 |
|
45 |
} |
|
46 |
||
47 |
||
48 |
## process command line |
|
49 |
||
50 |
# options |
|
51 |
||
52 |
ALL="" |
|
2902 | 53 |
BATCH="" |
6256 | 54 |
IMAGES="" |
2918 | 55 |
TEST="" |
2755 | 56 |
|
6256 | 57 |
while getopts "abit" OPT |
2879 | 58 |
do |
59 |
case "$OPT" in |
|
60 |
a) |
|
61 |
ALL=true |
|
62 |
;; |
|
2902 | 63 |
b) |
64 |
BATCH=true |
|
65 |
;; |
|
6256 | 66 |
i) |
67 |
IMAGES=images |
|
68 |
;; |
|
2918 | 69 |
t) |
70 |
TEST=test |
|
71 |
;; |
|
2879 | 72 |
\?) |
73 |
usage |
|
74 |
;; |
|
75 |
esac |
|
76 |
done |
|
77 |
||
78 |
shift $(($OPTIND - 1)) |
|
79 |
||
80 |
||
81 |
# args |
|
82 |
||
83 |
LOGICS="$@" |
|
84 |
||
4457 | 85 |
[ -n "$ALL" ] && LOGICS="$LOGICS $ALL_LOGICS" |
86 |
[ -z "$LOGICS" ] && LOGICS="$ISABELLE_LOGIC" |
|
87 |
||
2879 | 88 |
|
89 |
## main |
|
90 |
||
91 |
# tell the user about current values |
|
92 |
||
2902 | 93 |
if [ -z "$BATCH" ]; then |
94 |
echo |
|
95 |
echo " *****************************" |
|
96 |
echo " * Welcome to Isabelle build *" |
|
97 |
echo " *****************************" |
|
98 |
echo |
|
99 |
echo "Please check $ISABELLE_HOME/etc/settings" |
|
100 |
[ -f $ISABELLE_HOME_USER/etc/settings ] && echo "AND $ISABELLE_HOME_USER/etc/settings" |
|
5386 | 101 |
echo "to make sure that Isabelle's ML system settings and compilation options" |
102 |
echo "are appropriate." |
|
2902 | 103 |
echo |
5386 | 104 |
echo "The current values are:" |
2902 | 105 |
echo |
106 |
echo " ML_SYSTEM=$ML_SYSTEM" |
|
107 |
echo " ML_HOME=$ML_HOME" |
|
108 |
echo " ML_OPTIONS=$ML_OPTIONS" |
|
5386 | 109 |
echo |
110 |
echo " ISABELLE_USEDIR_OPTIONS=$ISABELLE_USEDIR_OPTIONS" |
|
2902 | 111 |
fi |
2789 | 112 |
|
113 |
||
2879 | 114 |
# check logics |
2755 | 115 |
|
2902 | 116 |
if [ -z "$BATCH" ]; then |
117 |
echo |
|
118 |
echo |
|
119 |
echo "Press RETURN to start compilation (including parents) of:" |
|
120 |
echo |
|
121 |
fi |
|
2879 | 122 |
|
4457 | 123 |
|
124 |
MAKE_LOGICS="" |
|
2879 | 125 |
|
4457 | 126 |
for L in $LOGICS |
127 |
do |
|
128 |
DIR=$ISABELLE_HOME/src/$L |
|
129 |
if [ -f $DIR/IsaMakefile ]; then |
|
130 |
MAKE_LOGICS="$MAKE_LOGICS $L" |
|
131 |
else |
|
132 |
echo "No such logic: $L" |
|
133 |
fi |
|
134 |
done |
|
135 |
||
2879 | 136 |
|
2902 | 137 |
if [ -z "$BATCH" ]; then |
4457 | 138 |
echo " " $MAKE_LOGICS |
2902 | 139 |
echo |
140 |
read |
|
141 |
else |
|
142 |
echo |
|
4457 | 143 |
echo "Isabelle build:" $MAKE_LOGICS |
2914 | 144 |
echo |
2902 | 145 |
echo "ML_SYSTEM=$ML_SYSTEM" |
146 |
echo "ML_HOME=$ML_HOME" |
|
147 |
echo "ML_OPTIONS=$ML_OPTIONS" |
|
148 |
echo |
|
5393 | 149 |
echo "ISABELLE_USEDIR_OPTIONS=$ISABELLE_USEDIR_OPTIONS" |
150 |
echo |
|
2902 | 151 |
fi |
2755 | 152 |
|
153 |
||
2879 | 154 |
# build it |
155 |
||
4457 | 156 |
SECONDS=0 |
2914 | 157 |
echo -n "Started at "; date |
158 |
||
2781 | 159 |
export THIS_IS_ISABELLE_BUILD=true |
2755 | 160 |
|
4457 | 161 |
for L in $MAKE_LOGICS |
2755 | 162 |
do |
6256 | 163 |
( cd $ISABELLE_HOME/src/$L; $ISATOOL make $IMAGES $TEST ) |
2755 | 164 |
done |
2902 | 165 |
|
2914 | 166 |
echo -n "Finished at "; date |
4457 | 167 |
|
168 |
ELAPSED=$($ISABELLE_HOME/lib/scripts/showtime $SECONDS) |
|
169 |
echo "$ELAPSED total elapsed time" |