author | blanchet |
Mon, 06 Dec 2010 13:29:23 +0100 | |
changeset 40996 | 63112be4a469 |
parent 34282 | 549969a7f582 |
child 43948 | 8f5add916a99 |
permissions | -rwxr-xr-x |
11391 | 1 |
#!/usr/bin/env bash |
2339 | 2 |
# |
9789 | 3 |
# Author: Markus Wenzel, TU Muenchen |
2339 | 4 |
# |
34282
549969a7f582
simplified build/bootstrap of Isabelle/Scala components -- avoid make;
wenzelm
parents:
31317
diff
changeset
|
5 |
# mk - build Isabelle/Pure. |
2339 | 6 |
# |
34282
549969a7f582
simplified build/bootstrap of Isabelle/Scala components -- avoid make;
wenzelm
parents:
31317
diff
changeset
|
7 |
# Requires proper Isabelle settings environment. |
2339 | 8 |
|
9 |
||
10 |
## diagnostics |
|
11 |
||
3774 | 12 |
function usage() |
13 |
{ |
|
14 |
echo |
|
15 |
echo "Usage: $PRG [OPTIONS]" |
|
16 |
echo |
|
17 |
echo " Make Pure Isabelle." |
|
18 |
echo |
|
21996 | 19 |
echo " -R DIR/FILE run RAW session" |
20 |
echo " -r build RAW image" |
|
3774 | 21 |
echo |
22 |
exit 1 |
|
23 |
} |
|
24 |
||
2339 | 25 |
function fail() |
26 |
{ |
|
27 |
echo "$1" >&2 |
|
28 |
exit 2 |
|
29 |
} |
|
30 |
||
31 |
||
3774 | 32 |
## process command line |
33 |
||
34 |
# options |
|
35 |
||
21996 | 36 |
RAW_SESSION="" |
3774 | 37 |
RAW="" |
38 |
||
21996 | 39 |
while getopts "R:r" OPT |
3774 | 40 |
do |
41 |
case "$OPT" in |
|
21996 | 42 |
R) |
43 |
RAW_SESSION="$OPTARG" |
|
10102 | 44 |
;; |
3774 | 45 |
r) |
46 |
RAW=true |
|
47 |
;; |
|
48 |
\?) |
|
49 |
usage |
|
50 |
;; |
|
51 |
esac |
|
52 |
done |
|
53 |
||
54 |
shift $(($OPTIND - 1)) |
|
55 |
||
56 |
||
57 |
# args |
|
58 |
||
9789 | 59 |
[ "$#" -ne 0 ] && usage |
3774 | 60 |
|
61 |
||
2339 | 62 |
## main |
63 |
||
4442 | 64 |
# get compatibility file |
65 |
||
9789 | 66 |
ML_SYSTEM_BASE=$(echo "$ML_SYSTEM" | cut -f1 -d-) |
16131 | 67 |
[ -z "$ML_SYSTEM" ] && fail "Missing ML_SYSTEM settings!" |
2339 | 68 |
|
69 |
COMPAT="" |
|
70 |
[ -f "ML-Systems/$ML_SYSTEM_BASE.ML" ] && COMPAT="ML-Systems/$ML_SYSTEM_BASE.ML" |
|
71 |
[ -f "ML-Systems/$ML_SYSTEM.ML" ] && COMPAT="ML-Systems/$ML_SYSTEM.ML" |
|
72 |
[ -z "$COMPAT" ] && fail "Missing compatibility file for ML system \"$ML_SYSTEM\"!" |
|
73 |
||
4442 | 74 |
|
75 |
# prepare log dir |
|
76 |
||
77 |
LOGDIR="$ISABELLE_OUTPUT/log" |
|
78 |
mkdir -p "$LOGDIR" |
|
79 |
||
80 |
||
81 |
# run isabelle |
|
82 |
||
18321
3414557c2dda
replaced lib/scripts/showtime by more advanced lib/scripts/timestart|stop.bash;
wenzelm
parents:
16376
diff
changeset
|
83 |
. "$ISABELLE_HOME/lib/scripts/timestart.bash" |
4442 | 84 |
|
21996 | 85 |
if [ -n "$RAW" ]; then |
86 |
ITEM="RAW" |
|
87 |
echo "Building $ITEM ..." |
|
88 |
LOG="$LOGDIR/$ITEM" |
|
89 |
||
28502 | 90 |
"$ISABELLE_PROCESS" \ |
21996 | 91 |
-e "val ml_system = \"$ML_SYSTEM\";" \ |
92 |
-e "val ml_platform = \"$ML_PLATFORM\";" \ |
|
93 |
-e "use\"$COMPAT\" handle _ => exit 1;" \ |
|
30592
a66fe59e0a26
RAW: provide dummy Isar.main to make tty work gracefully (with ML toplevel);
wenzelm
parents:
30204
diff
changeset
|
94 |
-e "structure Isar = struct fun main () = () end;" \ |
30611 | 95 |
-e "ml_prompts \"ML> \" \"ML# \";" \ |
21996 | 96 |
-q -w RAW_ML_SYSTEM RAW > "$LOG" 2>&1 |
97 |
RC="$?" |
|
98 |
elif [ -n "$RAW_SESSION" ]; then |
|
99 |
ITEM="RAW-$(basename $(dirname "$RAW_SESSION"))" |
|
22011 | 100 |
echo "Running $ITEM ..." |
21996 | 101 |
LOG="$LOGDIR/$ITEM" |
102 |
||
28502 | 103 |
"$ISABELLE_PROCESS" \ |
21996 | 104 |
-e "use\"$RAW_SESSION\" handle _ => exit 1;" \ |
105 |
-q RAW > "$LOG" 2>&1 |
|
106 |
RC="$?" |
|
107 |
else |
|
4442 | 108 |
ITEM="Pure" |
7277 | 109 |
echo "Building $ITEM ..." |
4442 | 110 |
LOG="$LOGDIR/$ITEM" |
111 |
||
28502 | 112 |
"$ISABELLE_PROCESS" \ |
3774 | 113 |
-e "val ml_system = \"$ML_SYSTEM\";" \ |
16376 | 114 |
-e "val ml_platform = \"$ML_PLATFORM\";" \ |
4495 | 115 |
-e "(use\"$COMPAT\"; use\"ROOT.ML\") handle _ => exit 1;" \ |
30611 | 116 |
-e "ml_prompts \"ML> \" \"ML# \";" \ |
31317
1f5740424c69
removed "compress" option from isabelle-process and isabelle usedir -- this is always enabled;
wenzelm
parents:
30611
diff
changeset
|
117 |
-f -q -w RAW_ML_SYSTEM Pure > "$LOG" 2>&1 |
9789 | 118 |
RC="$?" |
3774 | 119 |
fi |
4442 | 120 |
|
18321
3414557c2dda
replaced lib/scripts/showtime by more advanced lib/scripts/timestart|stop.bash;
wenzelm
parents:
16376
diff
changeset
|
121 |
. "$ISABELLE_HOME/lib/scripts/timestop.bash" |
4442 | 122 |
|
123 |
||
124 |
# exit status |
|
125 |
||
9789 | 126 |
if [ "$RC" -eq 0 ]; then |
18321
3414557c2dda
replaced lib/scripts/showtime by more advanced lib/scripts/timestart|stop.bash;
wenzelm
parents:
16376
diff
changeset
|
127 |
echo "Finished $ITEM ($TIMES_REPORT)" |
4442 | 128 |
gzip --force "$LOG" |
129 |
else |
|
7263 | 130 |
echo "$ITEM FAILED" |
4442 | 131 |
echo "(see also $LOG)" |
9789 | 132 |
echo; tail "$LOG"; echo |
4442 | 133 |
fi |
134 |
||
9789 | 135 |
exit "$RC" |