49 shift $(($OPTIND - 1)) |
51 shift $(($OPTIND - 1)) |
50 |
52 |
51 |
53 |
52 # args |
54 # args |
53 |
55 |
54 [ $# -ne 0 ] && usage |
56 [ "$#" -ne 0 ] && usage |
55 |
57 |
56 |
58 |
57 ## main |
59 ## main |
58 |
60 |
59 # get compatibility file |
61 # get compatibility file |
60 |
62 |
61 ML_SYSTEM_BASE=$(echo $ML_SYSTEM | cut -f1 -d-) |
63 ML_SYSTEM_BASE=$(echo "$ML_SYSTEM" | cut -f1 -d-) |
62 [ -z "$ML_SYSTEM" ] && \ |
64 [ -z "$ML_SYSTEM" ] && \ |
63 fail "Missing ML system settings! Probably not run via 'isatool make'." |
65 fail "Missing ML system settings! Probably not run via 'isatool make'." |
64 |
66 |
65 COMPAT="" |
67 COMPAT="" |
66 [ -f "ML-Systems/$ML_SYSTEM_BASE.ML" ] && COMPAT="ML-Systems/$ML_SYSTEM_BASE.ML" |
68 [ -f "ML-Systems/$ML_SYSTEM_BASE.ML" ] && COMPAT="ML-Systems/$ML_SYSTEM_BASE.ML" |
81 if [ -z "$RAW" ]; then |
83 if [ -z "$RAW" ]; then |
82 ITEM="Pure" |
84 ITEM="Pure" |
83 echo "Building $ITEM ..." |
85 echo "Building $ITEM ..." |
84 LOG="$LOGDIR/$ITEM" |
86 LOG="$LOGDIR/$ITEM" |
85 |
87 |
86 $ISABELLE \ |
88 "$ISABELLE" \ |
87 -e "val ml_system = \"$ML_SYSTEM\";" \ |
89 -e "val ml_system = \"$ML_SYSTEM\";" \ |
88 -e "(use\"$COMPAT\"; use\"ROOT.ML\") handle _ => exit 1;" \ |
90 -e "(use\"$COMPAT\"; use\"ROOT.ML\") handle _ => exit 1;" \ |
89 -c -q -w RAW_ML_SYSTEM Pure > $LOG 2>&1 |
91 -c -q -w RAW_ML_SYSTEM Pure > "$LOG" 2>&1 |
90 RC=$? |
92 RC="$?" |
91 else |
93 else |
92 ITEM="RAW" |
94 ITEM="RAW" |
93 echo "Building $ITEM ..." |
95 echo "Building $ITEM ..." |
94 LOG="$LOGDIR/$ITEM" |
96 LOG="$LOGDIR/$ITEM" |
95 |
97 |
96 $ISABELLE \ |
98 "$ISABELLE" \ |
97 -e "val ml_system = \"$ML_SYSTEM\";" \ |
99 -e "val ml_system = \"$ML_SYSTEM\";" \ |
98 -e "use\"$COMPAT\" handle _ => exit 1;;" \ |
100 -e "use\"$COMPAT\" handle _ => exit 1;;" \ |
99 -q -w RAW_ML_SYSTEM RAW > $LOG 2>&1 |
101 -q -w RAW_ML_SYSTEM RAW > "$LOG" 2>&1 |
100 RC=$? |
102 RC="$?" |
101 fi |
103 fi |
102 |
104 |
103 ELAPSED=$($ISABELLE_HOME/lib/scripts/showtime $SECONDS) |
105 ELAPSED=$("$ISABELLE_HOME/lib/scripts/showtime" "$SECONDS") |
104 |
106 |
105 |
107 |
106 # exit status |
108 # exit status |
107 |
109 |
108 if [ $RC -eq 0 ]; then |
110 if [ "$RC" -eq 0 ]; then |
109 echo "Finished $ITEM ($ELAPSED elapsed time)" |
111 echo "Finished $ITEM ($ELAPSED elapsed time)" |
110 gzip --force "$LOG" |
112 gzip --force "$LOG" |
111 else |
113 else |
112 echo "$ITEM FAILED" |
114 echo "$ITEM FAILED" |
113 echo "(see also $LOG)" |
115 echo "(see also $LOG)" |
114 echo; tail $LOG; echo |
116 echo; tail "$LOG"; echo |
115 fi |
117 fi |
116 |
118 |
117 exit $RC |
119 exit "$RC" |