equal
deleted
inserted
replaced
4 # Author: Markus Wenzel, TU Muenchen |
4 # Author: Markus Wenzel, TU Muenchen |
5 # License: GPL (GNU GENERAL PUBLIC LICENSE) |
5 # License: GPL (GNU GENERAL PUBLIC LICENSE) |
6 # |
6 # |
7 # mk - build Pure Isabelle. |
7 # mk - build Pure Isabelle. |
8 # |
8 # |
9 # Assumes to be called via Isabelle make utility (cf. IsaMakefile). |
9 # Requires proper Isabelle settings environment (cf. IsaMakefile). |
10 |
10 |
11 |
11 |
12 ## diagnostics |
12 ## diagnostics |
13 |
13 |
14 function usage() |
14 function usage() |
16 echo |
16 echo |
17 echo "Usage: $PRG [OPTIONS]" |
17 echo "Usage: $PRG [OPTIONS]" |
18 echo |
18 echo |
19 echo " Make Pure Isabelle." |
19 echo " Make Pure Isabelle." |
20 echo |
20 echo |
21 echo " -r just prepare RAW image" |
21 echo " -C tell ML system to copy output image" |
|
22 echo " -r prepare RAW image only" |
22 echo |
23 echo |
23 exit 1 |
24 exit 1 |
24 } |
25 } |
25 |
26 |
26 function fail() |
27 function fail() |
32 |
33 |
33 ## process command line |
34 ## process command line |
34 |
35 |
35 # options |
36 # options |
36 |
37 |
|
38 COPY="" |
37 RAW="" |
39 RAW="" |
38 |
40 |
39 while getopts "r" OPT |
41 while getopts "Cr" OPT |
40 do |
42 do |
41 case "$OPT" in |
43 case "$OPT" in |
|
44 C) |
|
45 COPY="-C" |
|
46 ;; |
42 r) |
47 r) |
43 RAW=true |
48 RAW=true |
44 ;; |
49 ;; |
45 \?) |
50 \?) |
46 usage |
51 usage |
83 if [ -z "$RAW" ]; then |
88 if [ -z "$RAW" ]; then |
84 ITEM="Pure" |
89 ITEM="Pure" |
85 echo "Building $ITEM ..." |
90 echo "Building $ITEM ..." |
86 LOG="$LOGDIR/$ITEM" |
91 LOG="$LOGDIR/$ITEM" |
87 |
92 |
88 "$ISABELLE" \ |
93 "$ISABELLE" $COPY \ |
89 -e "val ml_system = \"$ML_SYSTEM\";" \ |
94 -e "val ml_system = \"$ML_SYSTEM\";" \ |
90 -e "(use\"$COMPAT\"; use\"ROOT.ML\") handle _ => exit 1;" \ |
95 -e "(use\"$COMPAT\"; use\"ROOT.ML\") handle _ => exit 1;" \ |
91 -c -q -w RAW_ML_SYSTEM Pure > "$LOG" 2>&1 |
96 -c -q -w RAW_ML_SYSTEM Pure > "$LOG" 2>&1 |
92 RC="$?" |
97 RC="$?" |
93 else |
98 else |
94 ITEM="RAW" |
99 ITEM="RAW" |
95 echo "Building $ITEM ..." |
100 echo "Building $ITEM ..." |
96 LOG="$LOGDIR/$ITEM" |
101 LOG="$LOGDIR/$ITEM" |
97 |
102 |
98 "$ISABELLE" \ |
103 "$ISABELLE" $COPY \ |
99 -e "val ml_system = \"$ML_SYSTEM\";" \ |
104 -e "val ml_system = \"$ML_SYSTEM\";" \ |
100 -e "use\"$COMPAT\" handle _ => exit 1;;" \ |
105 -e "use\"$COMPAT\" handle _ => exit 1;;" \ |
101 -q -w RAW_ML_SYSTEM RAW > "$LOG" 2>&1 |
106 -q -w RAW_ML_SYSTEM RAW > "$LOG" 2>&1 |
102 RC="$?" |
107 RC="$?" |
103 fi |
108 fi |