lib/Tools/makeall
author kleing
Fri Jun 21 12:35:33 2002 +0200 (2002-06-21 ago)
changeset 13235 c26fc3baeffc
parent 13229 a2b09d99e5cf
child 13834 4d50cf8ea3d7
permissions -rwxr-xr-x
fail not so early, but produce correct exit code in the end
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@2502
    27
kleing@13229
    28
function fail()
kleing@13229
    29
{
kleing@13229
    30
  echo "$1" >&2
kleing@13229
    31
  exit 2
kleing@13229
    32
}
wenzelm@2502
    33
wenzelm@4456
    34
## main
wenzelm@4456
    35
wenzelm@4456
    36
[ "$1" = "-?" ] && usage
wenzelm@2502
    37
kleing@13235
    38
FAIL=""
kleing@13235
    39
wenzelm@10511
    40
echo "Started at $(date) ($ML_IDENTIFIER on $(hostname))"
wenzelm@2502
    41
wenzelm@4456
    42
for L in $ALL_LOGICS
wenzelm@4456
    43
do
kleing@13235
    44
  ( cd "$ISABELLE_HOME/src/$L"; "$ISATOOL" make "$@" ) || FAIL="$FAIL$L "
wenzelm@4456
    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@13235
    52
[ "$FAIL" == "" ] || fail "Logics ${FAIL}FAILED!"