65 |
70 |
66 ## main |
71 ## main |
67 |
72 |
68 # tell the user about current values |
73 # tell the user about current values |
69 |
74 |
70 echo |
75 if [ -z "$BATCH" ]; then |
71 echo " *****************************" |
76 echo |
72 echo " * Welcome to Isabelle build *" |
77 echo " *****************************" |
73 echo " *****************************" |
78 echo " * Welcome to Isabelle build *" |
74 echo |
79 echo " *****************************" |
75 echo "Please check $ISABELLE_HOME/etc/settings" |
80 echo |
76 [ -f $ISABELLE_HOME_USER/etc/settings ] && echo "AND $ISABELLE_HOME_USER/etc/settings" |
81 echo "Please check $ISABELLE_HOME/etc/settings" |
77 echo "to make sure that Isabelle's ML system settings are appropriate." |
82 [ -f $ISABELLE_HOME_USER/etc/settings ] && echo "AND $ISABELLE_HOME_USER/etc/settings" |
78 echo |
83 echo "to make sure that Isabelle's ML system settings are appropriate." |
79 echo "Your current values are:" |
84 echo |
80 echo |
85 echo "Your current values are:" |
81 |
86 echo |
82 echo " ML_SYSTEM=$ML_SYSTEM" |
87 echo " ML_SYSTEM=$ML_SYSTEM" |
83 echo " ML_HOME=$ML_HOME" |
88 echo " ML_HOME=$ML_HOME" |
84 echo " ML_OPTIONS=$ML_OPTIONS" |
89 echo " ML_OPTIONS=$ML_OPTIONS" |
|
90 fi |
85 |
91 |
86 |
92 |
87 # check logics |
93 # check logics |
88 |
94 |
89 echo |
95 if [ -z "$BATCH" ]; then |
90 echo |
96 echo |
91 echo "Press RETURN to start compilation (including parents) of:" |
97 echo |
92 echo |
98 echo "Press RETURN to start compilation (including parents) of:" |
|
99 echo |
|
100 fi |
93 |
101 |
94 [ -z "$LOGICS" ] && LOGICS=$DEFAULT_LOGIC |
102 [ -z "$LOGICS" ] && LOGICS=$DEFAULT_LOGIC |
95 |
103 |
96 if [ -n "$ALL" ]; then |
104 if [ -n "$ALL" ]; then |
97 LOGICS="" |
105 LOGICS="" |
108 DIR=$ISABELLE_HOME/src/$L |
116 DIR=$ISABELLE_HOME/src/$L |
109 [ ! -f $DIR/IsaMakefile ] && fail "No such logic: $L" |
117 [ ! -f $DIR/IsaMakefile ] && fail "No such logic: $L" |
110 done |
118 done |
111 fi |
119 fi |
112 |
120 |
113 echo " " $LOGICS |
121 if [ -z "$BATCH" ]; then |
114 echo |
122 echo " " $LOGICS |
115 read |
123 echo |
|
124 read |
|
125 else |
|
126 echo |
|
127 echo -n "Isabelle build started at "; date |
|
128 echo "logics:" $LOGICS |
|
129 echo "ML_SYSTEM=$ML_SYSTEM" |
|
130 echo "ML_HOME=$ML_HOME" |
|
131 echo "ML_OPTIONS=$ML_OPTIONS" |
|
132 echo |
|
133 fi |
116 |
134 |
117 |
135 |
118 # build it |
136 # build it |
119 |
137 |
120 export THIS_IS_ISABELLE_BUILD=true |
138 export THIS_IS_ISABELLE_BUILD=true |
121 |
139 |
122 for L in $LOGICS |
140 for L in $LOGICS |
123 do |
141 do |
124 ( cd $ISABELLE_HOME/src/$L; $ISATOOL make ) |
142 ( cd $ISABELLE_HOME/src/$L; $ISATOOL make ) |
125 done |
143 done |
|
144 |
|
145 if [ -n "$BATCH" ]; then |
|
146 echo |
|
147 echo -n "Isabelle build finished at "; date |
|
148 fi |