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