author | kleing |
Wed, 26 Feb 2003 14:26:18 +0100 | |
changeset 13834 | 4d50cf8ea3d7 |
parent 13235 | c26fc3baeffc |
child 14281 | a8c4a1e63071 |
permissions | -rwxr-xr-x |
wenzelm@10555 | 1 |
#!/usr/bin/env bash |
wenzelm@2502 | 2 |
# |
wenzelm@2502 | 3 |
# $Id$ |
wenzelm@9788 | 4 |
# Author: Markus Wenzel, TU Muenchen |
wenzelm@9788 | 5 |
# License: GPL (GNU GENERAL PUBLIC LICENSE) |
wenzelm@2502 | 6 |
# |
wenzelm@4456 | 7 |
# DESCRIPTION: apply make utility to all logics |
wenzelm@2502 | 8 |
|
wenzelm@4456 | 9 |
## global settings |
wenzelm@2502 | 10 |
|
wenzelm@4456 | 11 |
ALL_LOGICS="CCL CTT Cube FOL FOLP HOL HOLCF LCF Pure Sequents ZF" |
wenzelm@2502 | 12 |
|
wenzelm@2502 | 13 |
|
wenzelm@4456 | 14 |
## diagnostics |
wenzelm@2502 | 15 |
|
wenzelm@10511 | 16 |
PRG="$(basename "$0")" |
wenzelm@2502 | 17 |
|
wenzelm@4456 | 18 |
function usage() |
wenzelm@4456 | 19 |
{ |
wenzelm@4456 | 20 |
echo |
wenzelm@4456 | 21 |
echo "Usage: $PRG [ARGS ...]" |
wenzelm@4456 | 22 |
echo |
wenzelm@4456 | 23 |
echo " Apply isatool make to all logics (passing ARGS)." |
wenzelm@4456 | 24 |
echo |
wenzelm@4456 | 25 |
exit 1 |
wenzelm@4456 | 26 |
} |
wenzelm@4456 | 27 |
|
kleing@13229 | 28 |
function fail() |
kleing@13229 | 29 |
{ |
kleing@13229 | 30 |
echo "$1" >&2 |
kleing@13229 | 31 |
exit 2 |
kleing@13229 | 32 |
} |
wenzelm@4456 | 33 |
|
wenzelm@4456 | 34 |
## main |
wenzelm@4456 | 35 |
|
wenzelm@4456 | 36 |
[ "$1" = "-?" ] && usage |
wenzelm@4456 | 37 |
|
kleing@13235 | 38 |
FAIL="" |
kleing@13235 | 39 |
|
wenzelm@10511 | 40 |
echo "Started at $(date) ($ML_IDENTIFIER on $(hostname))" |
wenzelm@4456 | 41 |
|
wenzelm@4456 | 42 |
for L in $ALL_LOGICS |
wenzelm@2502 | 43 |
do |
kleing@13235 | 44 |
( cd "$ISABELLE_HOME/src/$L"; "$ISATOOL" make "$@" ) || FAIL="$FAIL$L " |
wenzelm@2502 | 45 |
done |
wenzelm@2502 | 46 |
|
wenzelm@4456 | 47 |
echo -n "Finished at "; date |
wenzelm@2502 | 48 |
|
wenzelm@9788 | 49 |
ELAPSED=$("$ISABELLE_HOME/lib/scripts/showtime" "$SECONDS") |
wenzelm@4456 | 50 |
echo "$ELAPSED total elapsed time" |
kleing@13235 | 51 |
|
kleing@13834 | 52 |
[ "$FAIL" = "" ] || fail "Logics ${FAIL}FAILED!" |