| author | wenzelm |
| Tue, 04 Aug 2009 16:11:11 +0200 | |
| changeset 32325 | 300b7d5d23d7 |
| parent 29143 | 72c960b2b83e |
| child 32390 | 468eff174a77 |
| permissions | -rwxr-xr-x |
| wenzelm@10555 | 1 |
#!/usr/bin/env bash |
| wenzelm@2502 | 2 |
# |
| wenzelm@9788 | 3 |
# Author: Markus Wenzel, TU Muenchen |
| wenzelm@2502 | 4 |
# |
| wenzelm@4456 | 5 |
# DESCRIPTION: apply make utility to all logics |
| wenzelm@2502 | 6 |
|
| wenzelm@4456 | 7 |
## diagnostics |
| wenzelm@2502 | 8 |
|
| wenzelm@10511 | 9 |
PRG="$(basename "$0")" |
| wenzelm@2502 | 10 |
|
| wenzelm@4456 | 11 |
function usage() |
| wenzelm@4456 | 12 |
{
|
| wenzelm@4456 | 13 |
echo |
| wenzelm@28650 | 14 |
echo "Usage: isabelle $PRG [ARGS ...]" |
| wenzelm@4456 | 15 |
echo |
| wenzelm@32325 | 16 |
echo " Apply isabelle make to all components with IsaMakefile (passing ARGS)." |
| wenzelm@4456 | 17 |
echo |
| wenzelm@4456 | 18 |
exit 1 |
| wenzelm@4456 | 19 |
} |
| wenzelm@4456 | 20 |
|
| kleing@13229 | 21 |
function fail() |
| kleing@13229 | 22 |
{
|
| kleing@13229 | 23 |
echo "$1" >&2 |
| kleing@13229 | 24 |
exit 2 |
| kleing@13229 | 25 |
} |
| wenzelm@4456 | 26 |
|
| wenzelm@32325 | 27 |
|
| wenzelm@4456 | 28 |
## main |
| wenzelm@4456 | 29 |
|
| wenzelm@4456 | 30 |
[ "$1" = "-?" ] && usage |
| wenzelm@4456 | 31 |
|
| kleing@13235 | 32 |
FAIL="" |
| kleing@13235 | 33 |
|
| wenzelm@10511 | 34 |
echo "Started at $(date) ($ML_IDENTIFIER on $(hostname))" |
| wenzelm@18321 | 35 |
. "$ISABELLE_HOME/lib/scripts/timestart.bash" |
| wenzelm@4456 | 36 |
|
| wenzelm@32325 | 37 |
ORIG_IFS="$IFS"; IFS=":"; declare -a COMPONENTS=($ISABELLE_COMPONENTS); IFS="$ORIG_IFS" |
| wenzelm@32325 | 38 |
|
| wenzelm@32325 | 39 |
for DIR in "${COMPONENTS[@]}"
|
| wenzelm@2502 | 40 |
do |
| wenzelm@32325 | 41 |
if [ -f "$DIR/IsaMakefile" ]; then |
| wenzelm@32325 | 42 |
NAME="$(basename "$DIR")" |
| wenzelm@32325 | 43 |
( cd "$DIR"; "$ISABELLE_TOOL" make "$@" ) || FAIL="$FAIL$NAME " |
| wenzelm@32325 | 44 |
fi |
| wenzelm@2502 | 45 |
done |
| wenzelm@2502 | 46 |
|
| wenzelm@4456 | 47 |
echo -n "Finished at "; date |
| wenzelm@2502 | 48 |
|
| wenzelm@18321 | 49 |
. "$ISABELLE_HOME/lib/scripts/timestop.bash" |
| wenzelm@18321 | 50 |
echo "$TIMES_REPORT" |
| kleing@13235 | 51 |
|
| kleing@13834 | 52 |
[ "$FAIL" = "" ] || fail "Logics ${FAIL}FAILED!"
|