author | wenzelm |
Mon, 29 Feb 2016 16:31:50 +0100 | |
changeset 62473 | b883960a4c03 |
parent 62472 | 01e2bd5b4027 |
permissions | -rwxr-xr-x |
48360 | 1 |
#!/usr/bin/env bash |
2 |
# |
|
3 |
# Author: Makarius |
|
4 |
# |
|
5 |
# build - build Isabelle/ML |
|
6 |
# |
|
7 |
# Requires proper Isabelle settings environment. |
|
8 |
||
9 |
||
10 |
## diagnostics |
|
11 |
||
12 |
function usage() |
|
13 |
{ |
|
14 |
echo |
|
48511
37999ee01156
remove old output heaps, to ensure that result is valid wrt. check_stamps;
wenzelm
parents:
48447
diff
changeset
|
15 |
echo "Usage: $PRG TARGET [OUTPUT]" |
48360 | 16 |
echo |
17 |
exit 1 |
|
18 |
} |
|
19 |
||
20 |
function fail() |
|
21 |
{ |
|
22 |
echo "$1" >&2 |
|
23 |
exit 2 |
|
24 |
} |
|
25 |
||
26 |
[ -z "$ISABELLE_HOME" ] && fail "Missing Isabelle settings environment" |
|
27 |
||
28 |
||
29 |
## process command line |
|
30 |
||
48373 | 31 |
# args |
32 |
||
48511
37999ee01156
remove old output heaps, to ensure that result is valid wrt. check_stamps;
wenzelm
parents:
48447
diff
changeset
|
33 |
if [ "$#" -eq 1 ]; then |
37999ee01156
remove old output heaps, to ensure that result is valid wrt. check_stamps;
wenzelm
parents:
48447
diff
changeset
|
34 |
TARGET="$1"; shift |
37999ee01156
remove old output heaps, to ensure that result is valid wrt. check_stamps;
wenzelm
parents:
48447
diff
changeset
|
35 |
OUTPUT=""; shift |
37999ee01156
remove old output heaps, to ensure that result is valid wrt. check_stamps;
wenzelm
parents:
48447
diff
changeset
|
36 |
elif [ "$#" -eq 2 ]; then |
48447
ef600ce4559c
added system build mode: produce output in ISABELLE_HOME;
wenzelm
parents:
48417
diff
changeset
|
37 |
TARGET="$1"; shift |
ef600ce4559c
added system build mode: produce output in ISABELLE_HOME;
wenzelm
parents:
48417
diff
changeset
|
38 |
OUTPUT="$1"; shift |
ef600ce4559c
added system build mode: produce output in ISABELLE_HOME;
wenzelm
parents:
48417
diff
changeset
|
39 |
else |
ef600ce4559c
added system build mode: produce output in ISABELLE_HOME;
wenzelm
parents:
48417
diff
changeset
|
40 |
usage |
ef600ce4559c
added system build mode: produce output in ISABELLE_HOME;
wenzelm
parents:
48417
diff
changeset
|
41 |
fi |
48360 | 42 |
|
43 |
||
44 |
## main |
|
45 |
||
46 |
# get compatibility file |
|
47 |
||
48 |
ML_SYSTEM_BASE=$(echo "$ML_SYSTEM" | cut -f1 -d-) |
|
49 |
[ -z "$ML_SYSTEM" ] && fail "Missing ML_SYSTEM settings!" |
|
50 |
||
51 |
COMPAT="" |
|
62077 | 52 |
[ -f "RAW/ROOT_${ML_SYSTEM_BASE}.ML" ] && COMPAT="RAW/ROOT_${ML_SYSTEM_BASE}.ML" |
53 |
[ -f "RAW/ROOT_${ML_SYSTEM}.ML" ] && COMPAT="RAW/ROOT_${ML_SYSTEM}.ML" |
|
48360 | 54 |
[ -z "$COMPAT" ] && fail "Missing compatibility file for ML system \"$ML_SYSTEM\"!" |
55 |
||
56 |
||
57 |
# run isabelle |
|
58 |
||
59 |
. "$ISABELLE_HOME/lib/scripts/timestart.bash" |
|
60 |
||
48373 | 61 |
if [ "$TARGET" = RAW ]; then |
48447
ef600ce4559c
added system build mode: produce output in ISABELLE_HOME;
wenzelm
parents:
48417
diff
changeset
|
62 |
if [ -z "$OUTPUT" ]; then |
48373 | 63 |
"$ISABELLE_PROCESS" \ |
60962
faa452d8e265
basic setup for native Windows (RAW session without image);
wenzelm
parents:
52083
diff
changeset
|
64 |
-e "use \"$COMPAT\" handle _ => OS.Process.exit OS.Process.failure;" \ |
48373 | 65 |
-q RAW_ML_SYSTEM |
66 |
else |
|
62469 | 67 |
rm -f "$OUTPUT" |
48373 | 68 |
"$ISABELLE_PROCESS" \ |
60962
faa452d8e265
basic setup for native Windows (RAW session without image);
wenzelm
parents:
52083
diff
changeset
|
69 |
-e "use \"$COMPAT\" handle _ => OS.Process.exit OS.Process.failure;" \ |
62469 | 70 |
-e "ML_Heap.share_common_data (); ML_Heap.save_state \"$OUTPUT\";" \ |
71 |
-q RAW_ML_SYSTEM && chmod -w "$OUTPUT" |
|
48373 | 72 |
fi |
73 |
else |
|
48447
ef600ce4559c
added system build mode: produce output in ISABELLE_HOME;
wenzelm
parents:
48417
diff
changeset
|
74 |
if [ -z "$OUTPUT" ]; then |
48373 | 75 |
"$ISABELLE_PROCESS" \ |
60962
faa452d8e265
basic setup for native Windows (RAW session without image);
wenzelm
parents:
52083
diff
changeset
|
76 |
-e "(use \"$COMPAT\"; use \"ROOT.ML\") handle _ => OS.Process.exit OS.Process.failure;" \ |
48373 | 77 |
-q RAW_ML_SYSTEM |
78 |
else |
|
62469 | 79 |
rm -f "$OUTPUT" |
48373 | 80 |
"$ISABELLE_PROCESS" \ |
60962
faa452d8e265
basic setup for native Windows (RAW session without image);
wenzelm
parents:
52083
diff
changeset
|
81 |
-e "(use \"$COMPAT\"; use \"ROOT.ML\") handle _ => OS.Process.exit OS.Process.failure;" \ |
62470
9037ed690e19
proper exit as in Scala version (in contrast to a45ba78abcc1);
wenzelm
parents:
62469
diff
changeset
|
82 |
-e "Command_Line.tool0 (fn () => (Session.finish (); Options.reset_default (); Session.shutdown (); ML_Heap.share_common_data (); ML_Heap.save_state \"$OUTPUT\"));" \ |
62469 | 83 |
-q RAW_ML_SYSTEM && chmod -w "$OUTPUT" |
48373 | 84 |
fi |
85 |
fi |
|
48360 | 86 |
|
48373 | 87 |
RC="$?" |
48360 | 88 |
|
89 |
. "$ISABELLE_HOME/lib/scripts/timestop.bash" |
|
90 |
||
91 |
if [ "$RC" -eq 0 ]; then |
|
92 |
echo "Finished $TARGET ($TIMES_REPORT)" >&2 |
|
93 |
fi |
|
94 |
||
95 |
exit "$RC" |