tuned;
authorwenzelm
Fri Dec 19 12:16:32 1997 +0100 (1997-12-19)
changeset 44576e6d99e06d0c
parent 4456 44e57a6d947d
child 4458 ad8be126603d
tuned;
build
     1.1 --- a/build	Fri Dec 19 12:09:58 1997 +0100
     1.2 +++ b/build	Fri Dec 19 12:16:32 1997 +0100
     1.3 @@ -5,6 +5,11 @@
     1.4  # build - compile the Isabelle system and object-logics
     1.5  
     1.6  
     1.7 +## global settings
     1.8 +
     1.9 +ALL_LOGICS="CCL CTT Cube FOL FOLP HOL HOLCF LCF Pure Sequents ZF"
    1.10 +
    1.11 +
    1.12  ## settings
    1.13  
    1.14  PRG=$(basename $0)
    1.15 @@ -72,6 +77,9 @@
    1.16  
    1.17  LOGICS="$@"
    1.18  
    1.19 +[ -n "$ALL" ] && LOGICS="$LOGICS $ALL_LOGICS"
    1.20 +[ -z "$LOGICS" ] && LOGICS="$ISABELLE_LOGIC"
    1.21 +
    1.22  
    1.23  ## main
    1.24  
    1.25 @@ -104,32 +112,27 @@
    1.26    echo
    1.27  fi
    1.28  
    1.29 -[ -z "$LOGICS" ] && LOGICS=$ISABELLE_LOGIC
    1.30 +
    1.31 +MAKE_LOGICS=""
    1.32  
    1.33 -if [ -n "$ALL" ]; then
    1.34 -  LOGICS=""
    1.35 -  for DIR in $ISABELLE_HOME/src/*
    1.36 -  do
    1.37 -    if [ -f $DIR/IsaMakefile ]; then
    1.38 -      L=$(basename $DIR)
    1.39 -      LOGICS="$LOGICS $L"
    1.40 -    fi
    1.41 -  done
    1.42 -else
    1.43 -  for L in $LOGICS
    1.44 -  do
    1.45 -    DIR=$ISABELLE_HOME/src/$L
    1.46 -    [ ! -f $DIR/IsaMakefile ] && fail "No such logic: $L"
    1.47 -  done
    1.48 -fi
    1.49 +for L in $LOGICS
    1.50 +do
    1.51 +  DIR=$ISABELLE_HOME/src/$L
    1.52 +  if [ -f $DIR/IsaMakefile ]; then
    1.53 +    MAKE_LOGICS="$MAKE_LOGICS $L"
    1.54 +  else
    1.55 +    echo "No such logic: $L"
    1.56 +  fi
    1.57 +done
    1.58 +
    1.59  
    1.60  if [ -z "$BATCH" ]; then
    1.61 -  echo " " $LOGICS
    1.62 +  echo " " $MAKE_LOGICS
    1.63    echo
    1.64    read
    1.65  else
    1.66    echo
    1.67 -  echo "Isabelle build:" $LOGICS
    1.68 +  echo "Isabelle build:" $MAKE_LOGICS
    1.69    echo
    1.70    echo "ML_SYSTEM=$ML_SYSTEM"
    1.71    echo "ML_HOME=$ML_HOME"
    1.72 @@ -140,17 +143,17 @@
    1.73  
    1.74  # build it
    1.75  
    1.76 -echo
    1.77 +SECONDS=0
    1.78  echo -n "Started at "; date
    1.79 -echo
    1.80  
    1.81  export THIS_IS_ISABELLE_BUILD=true
    1.82  
    1.83 -for L in $LOGICS
    1.84 +for L in $MAKE_LOGICS
    1.85  do
    1.86    ( cd $ISABELLE_HOME/src/$L; $ISATOOL make $TEST )
    1.87  done
    1.88  
    1.89 -echo
    1.90  echo -n "Finished at "; date
    1.91 -echo
    1.92 +
    1.93 +ELAPSED=$($ISABELLE_HOME/lib/scripts/showtime $SECONDS)
    1.94 +echo "$ELAPSED total elapsed time"