10555
|
1 |
#!/usr/bin/env bash
|
2755
|
2 |
#
|
|
3 |
# $Id$
|
9817
|
4 |
# Author: Markus Wenzel, TU Muenchen
|
2755
|
5 |
#
|
2902
|
6 |
# build - compile the Isabelle system and object-logics
|
2755
|
7 |
|
15844
|
8 |
if [ -L "$0" ]; then
|
|
9 |
TARGET="$(LC_ALL=C ls -l "$0" | sed 's/.* -> //')"
|
15967
|
10 |
exec "$(cd "$(dirname "$0")"; cd "$(pwd -P)"; cd "$(dirname "$TARGET")"; pwd)/$(basename "$TARGET")" "$@"
|
15844
|
11 |
fi
|
|
12 |
|
2755
|
13 |
|
4457
|
14 |
## global settings
|
|
15 |
|
15844
|
16 |
ALL_LOGICS="Pure FOL HOL ZF CCL CTT Cube FOLP HOLCF LCF Sequents"
|
4457
|
17 |
|
|
18 |
|
2789
|
19 |
## settings
|
|
20 |
|
7889
|
21 |
export THIS_IS_ISABELLE_BUILD=true
|
15844
|
22 |
|
15967
|
23 |
PRG="$(basename "$0")"
|
|
24 |
|
|
25 |
ISABELLE_HOME="$(cd "$(dirname "$0")"; pwd -P)"
|
|
26 |
source "$ISABELLE_HOME/lib/scripts/getsettings" || exit 2
|
2755
|
27 |
|
2789
|
28 |
|
2879
|
29 |
## diagnostics
|
|
30 |
|
|
31 |
function usage()
|
|
32 |
{
|
|
33 |
echo
|
|
34 |
echo "Usage: $PRG [OPTIONS] [LOGICS ...]"
|
|
35 |
echo
|
|
36 |
echo " Options are:"
|
|
37 |
echo " -a all logics"
|
2902
|
38 |
echo " -b batch mode"
|
6256
|
39 |
echo " -i make images"
|
7889
|
40 |
echo " -m TARGET make this target"
|
6256
|
41 |
echo " -t make test"
|
2879
|
42 |
echo
|
3184
|
43 |
echo " Compile the named LOGICS (default $ISABELLE_LOGIC), or all object logics"
|
2879
|
44 |
echo " in the distribution."
|
|
45 |
echo
|
|
46 |
exit 1
|
|
47 |
}
|
|
48 |
|
|
49 |
function fail()
|
|
50 |
{
|
|
51 |
echo "$1" >&2
|
|
52 |
exit 2
|
|
53 |
}
|
|
54 |
|
|
55 |
|
|
56 |
## process command line
|
|
57 |
|
|
58 |
# options
|
|
59 |
|
|
60 |
ALL=""
|
2902
|
61 |
BATCH=""
|
7889
|
62 |
TARGETS=""
|
2755
|
63 |
|
15844
|
64 |
while getopts "abim:t" OPT
|
2879
|
65 |
do
|
|
66 |
case "$OPT" in
|
|
67 |
a)
|
|
68 |
ALL=true
|
|
69 |
;;
|
2902
|
70 |
b)
|
|
71 |
BATCH=true
|
|
72 |
;;
|
6256
|
73 |
i)
|
7889
|
74 |
TARGETS="$TARGETS images"
|
|
75 |
;;
|
|
76 |
m)
|
|
77 |
TARGETS="$TARGETS $OPTARG"
|
6256
|
78 |
;;
|
2918
|
79 |
t)
|
7889
|
80 |
TARGETS="$TARGETS test"
|
2918
|
81 |
;;
|
2879
|
82 |
\?)
|
|
83 |
usage
|
|
84 |
;;
|
|
85 |
esac
|
|
86 |
done
|
|
87 |
|
|
88 |
shift $(($OPTIND - 1))
|
|
89 |
|
|
90 |
|
|
91 |
# args
|
|
92 |
|
|
93 |
LOGICS="$@"
|
|
94 |
|
4457
|
95 |
[ -n "$ALL" ] && LOGICS="$LOGICS $ALL_LOGICS"
|
|
96 |
[ -z "$LOGICS" ] && LOGICS="$ISABELLE_LOGIC"
|
|
97 |
|
2879
|
98 |
|
|
99 |
## main
|
|
100 |
|
|
101 |
# tell the user about current values
|
|
102 |
|
2902
|
103 |
if [ -z "$BATCH" ]; then
|
|
104 |
echo
|
|
105 |
echo " *****************************"
|
|
106 |
echo " * Welcome to Isabelle build *"
|
|
107 |
echo " *****************************"
|
|
108 |
echo
|
|
109 |
echo "Please check $ISABELLE_HOME/etc/settings"
|
9789
|
110 |
[ -f "$ISABELLE_HOME_USER/etc/settings" ] && echo "AND $ISABELLE_HOME_USER/etc/settings"
|
5386
|
111 |
echo "to make sure that Isabelle's ML system settings and compilation options"
|
|
112 |
echo "are appropriate."
|
2902
|
113 |
echo
|
5386
|
114 |
echo "The current values are:"
|
2902
|
115 |
echo
|
|
116 |
echo " ML_SYSTEM=$ML_SYSTEM"
|
|
117 |
echo " ML_HOME=$ML_HOME"
|
|
118 |
echo " ML_OPTIONS=$ML_OPTIONS"
|
7277
|
119 |
echo " ML_PLATFORM=$ML_PLATFORM"
|
5386
|
120 |
echo
|
|
121 |
echo " ISABELLE_USEDIR_OPTIONS=$ISABELLE_USEDIR_OPTIONS"
|
2902
|
122 |
fi
|
2789
|
123 |
|
|
124 |
|
2879
|
125 |
# check logics
|
2755
|
126 |
|
2902
|
127 |
if [ -z "$BATCH" ]; then
|
|
128 |
echo
|
|
129 |
echo
|
9817
|
130 |
echo "Press RETURN to compilation of"
|
2902
|
131 |
echo
|
|
132 |
fi
|
2879
|
133 |
|
4457
|
134 |
|
|
135 |
MAKE_LOGICS=""
|
2879
|
136 |
|
4457
|
137 |
for L in $LOGICS
|
|
138 |
do
|
9789
|
139 |
DIR="$ISABELLE_HOME/src/$L"
|
|
140 |
if [ -f "$DIR/IsaMakefile" ]; then
|
4457
|
141 |
MAKE_LOGICS="$MAKE_LOGICS $L"
|
|
142 |
else
|
|
143 |
echo "No such logic: $L"
|
|
144 |
fi
|
|
145 |
done
|
|
146 |
|
2879
|
147 |
|
2902
|
148 |
if [ -z "$BATCH" ]; then
|
9789
|
149 |
echo " $MAKE_LOGICS"
|
9817
|
150 |
[ -n "$TARGETS" ] && echo " (targets:$TARGETS)"
|
2902
|
151 |
echo
|
|
152 |
read
|
|
153 |
else
|
|
154 |
echo
|
9789
|
155 |
echo "Isabelle build: $MAKE_LOGICS"
|
9817
|
156 |
[ -n "$TARGETS" ] && echo "(targets:$TARGETS)"
|
2914
|
157 |
echo
|
2902
|
158 |
echo "ML_SYSTEM=$ML_SYSTEM"
|
|
159 |
echo "ML_HOME=$ML_HOME"
|
|
160 |
echo "ML_OPTIONS=$ML_OPTIONS"
|
7311
|
161 |
echo "ML_PLATFORM=$ML_PLATFORM"
|
2902
|
162 |
echo
|
5393
|
163 |
echo "ISABELLE_USEDIR_OPTIONS=$ISABELLE_USEDIR_OPTIONS"
|
|
164 |
echo
|
2902
|
165 |
fi
|
2755
|
166 |
|
|
167 |
|
2879
|
168 |
# build it
|
|
169 |
|
4457
|
170 |
SECONDS=0
|
10511
|
171 |
echo "Started at $(date) ($ML_IDENTIFIER on $(hostname))"
|
2914
|
172 |
|
4457
|
173 |
for L in $MAKE_LOGICS
|
2755
|
174 |
do
|
14056
|
175 |
( cd "$ISABELLE_HOME/src/$L"; "$ISATOOL" make $TARGETS )
|
2755
|
176 |
done
|
2902
|
177 |
|
2914
|
178 |
echo -n "Finished at "; date
|
4457
|
179 |
|
9789
|
180 |
ELAPSED=$("$ISABELLE_HOME/lib/scripts/showtime" "$SECONDS")
|
4457
|
181 |
echo "$ELAPSED total elapsed time"
|