author | wenzelm |
Mon, 23 Jul 2012 15:59:14 +0200 | |
changeset 48447 | ef600ce4559c |
parent 48417 | bb1d4ec90f30 |
child 48511 | 37999ee01156 |
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 |
|
48447
ef600ce4559c
added system build mode: produce output in ISABELLE_HOME;
wenzelm
parents:
48417
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 |
||
48447
ef600ce4559c
added system build mode: produce output in ISABELLE_HOME;
wenzelm
parents:
48417
diff
changeset
|
33 |
if [ "$#" -eq 2 ]; then |
ef600ce4559c
added system build mode: produce output in ISABELLE_HOME;
wenzelm
parents:
48417
diff
changeset
|
34 |
TARGET="$1"; shift |
ef600ce4559c
added system build mode: produce output in ISABELLE_HOME;
wenzelm
parents:
48417
diff
changeset
|
35 |
OUTPUT="$1"; shift |
ef600ce4559c
added system build mode: produce output in ISABELLE_HOME;
wenzelm
parents:
48417
diff
changeset
|
36 |
else |
ef600ce4559c
added system build mode: produce output in ISABELLE_HOME;
wenzelm
parents:
48417
diff
changeset
|
37 |
usage |
ef600ce4559c
added system build mode: produce output in ISABELLE_HOME;
wenzelm
parents:
48417
diff
changeset
|
38 |
fi |
48360 | 39 |
|
40 |
||
41 |
## main |
|
42 |
||
43 |
# get compatibility file |
|
44 |
||
45 |
ML_SYSTEM_BASE=$(echo "$ML_SYSTEM" | cut -f1 -d-) |
|
46 |
[ -z "$ML_SYSTEM" ] && fail "Missing ML_SYSTEM settings!" |
|
47 |
||
48 |
COMPAT="" |
|
49 |
[ -f "ML-Systems/${ML_SYSTEM_BASE}.ML" ] && COMPAT="ML-Systems/${ML_SYSTEM_BASE}.ML" |
|
50 |
[ -f "ML-Systems/${ML_SYSTEM}.ML" ] && COMPAT="ML-Systems/${ML_SYSTEM}.ML" |
|
51 |
[ -z "$COMPAT" ] && fail "Missing compatibility file for ML system \"$ML_SYSTEM\"!" |
|
52 |
||
53 |
||
54 |
# run isabelle |
|
55 |
||
56 |
. "$ISABELLE_HOME/lib/scripts/timestart.bash" |
|
57 |
||
48373 | 58 |
if [ "$TARGET" = RAW ]; then |
48447
ef600ce4559c
added system build mode: produce output in ISABELLE_HOME;
wenzelm
parents:
48417
diff
changeset
|
59 |
if [ -z "$OUTPUT" ]; then |
48373 | 60 |
"$ISABELLE_PROCESS" \ |
48417 | 61 |
-e "use\"$COMPAT\" handle _ => OS.Process.exit OS.Process.failure;" \ |
48373 | 62 |
-q RAW_ML_SYSTEM |
63 |
else |
|
64 |
"$ISABELLE_PROCESS" \ |
|
48417 | 65 |
-e "use\"$COMPAT\" handle _ => OS.Process.exit OS.Process.failure;" \ |
48373 | 66 |
-e "structure Isar = struct fun main () = () end;" \ |
67 |
-e "ml_prompts \"ML> \" \"ML# \";" \ |
|
48447
ef600ce4559c
added system build mode: produce output in ISABELLE_HOME;
wenzelm
parents:
48417
diff
changeset
|
68 |
-q -w RAW_ML_SYSTEM "$OUTPUT" |
48373 | 69 |
fi |
70 |
else |
|
48447
ef600ce4559c
added system build mode: produce output in ISABELLE_HOME;
wenzelm
parents:
48417
diff
changeset
|
71 |
if [ -z "$OUTPUT" ]; then |
48373 | 72 |
"$ISABELLE_PROCESS" \ |
48417 | 73 |
-e "(use\"$COMPAT\"; use\"ROOT.ML\") handle _ => OS.Process.exit OS.Process.failure;" \ |
48373 | 74 |
-q RAW_ML_SYSTEM |
75 |
else |
|
76 |
"$ISABELLE_PROCESS" \ |
|
48417 | 77 |
-e "(use\"$COMPAT\"; use\"ROOT.ML\") handle _ => OS.Process.exit OS.Process.failure;" \ |
48373 | 78 |
-e "ml_prompts \"ML> \" \"ML# \";" \ |
48447
ef600ce4559c
added system build mode: produce output in ISABELLE_HOME;
wenzelm
parents:
48417
diff
changeset
|
79 |
-f -q -w RAW_ML_SYSTEM "$OUTPUT" |
48373 | 80 |
fi |
81 |
fi |
|
48360 | 82 |
|
48373 | 83 |
RC="$?" |
48360 | 84 |
|
85 |
. "$ISABELLE_HOME/lib/scripts/timestop.bash" |
|
86 |
||
87 |
if [ "$RC" -eq 0 ]; then |
|
88 |
echo "Finished $TARGET ($TIMES_REPORT)" >&2 |
|
89 |
fi |
|
90 |
||
91 |
exit "$RC" |