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