wneuper/isa: Admin/isatest/isatest-makeall@91c4d7397f0e

     1 #!/usr/bin/env bash

2 #

     3 # Author: Gerwin Klein, TU Muenchen

4 #

     5 # DESCRIPTION: Run isabelle makeall from specified distribution and settings.

     7 ## global settings

     8 . ~/admin/isatest/isatest-settings

    10 # max time until test is aborted (in sec)

    11 MAXTIME=28800

    13 PUBLISH_TEST="$HOME/home/isabelle-repository/repos/testtool/publish_test.py"

    15 ## diagnostics

    17 PRG="$(basename "$0")"

    19 function usage()

    20 {

    21   echo

    22   echo "Usage: $PRG [-l logic targets] settings1 [settings2 ...]"

    23   echo

    24   echo "  Runs isabelle makeall for specified settings."

    25   echo "  Leaves messages in ${ERRORLOG} and ${LOGPREFIX} if it fails."

    26   echo

    27   echo "Examples:"

    28   echo "  $PRG ~/settings/at-poly ~/settings/at-sml"

    29   echo "  $PRG -l HOL \"HOL-Library HOL-Bali\" ~/settings/at-poly"

    30   exit 1

    31 }

    33 function fail()

    34 {

    35   echo "$1" >&2

    36   log "FAILED, $1"

    37   exit 2

    38 }

    40 ## main

    42 # argument checking

    44 [ "$1" = "-?" ] && usage

    45 [ "$#" -lt "1" ] && usage

    47 [ -d $DISTPREFIX ] || fail "$DISTPREFIX is not a directory."

    49 # make file flags and nice setup for different target platforms

    50 case $HOSTNAME in

    51     atbroy51)

    52         MFLAGS="-k -j 2"

    53         NICE=""

    54         ;;

    56     atbroy98)

    57         MFLAGS="-k"

    58         NICE=""

    59         ;;

    61     atbroy102)

    62         MFLAGS="-k"

    63         NICE=""

    64         ;;

    66     atbroy31)

    67         MFLAGS="-k -j 2"

    68         ;;

    70     macbroy2)

    71         MFLAGS="-k"

    72         NICE=""

    73         ;;

    75     macbroy5)

    76         MFLAGS="-k -j 2"

    77         NICE=""

    78         ;;

    80     macbroy22)

    81         MFLAGS="-k"

    82         NICE=""

    83         ;;

    85     macbroy28)

    86         MFLAGS="-k -j 2"

    87         NICE="nice"

    88         ;;

    90     macbroy2[0-9])

    91         MFLAGS="-k -j 2"

    92         NICE=""

    93         ;;

    95     *)

    96         MFLAGS="-k"

    97         # be nice by default

    98         NICE=nice

    99         ;;

   100 esac

   102 ISABELLE_TOOL="$DISTPREFIX/Isabelle/bin/isabelle"

   104 [ -x $ISABELLE_TOOL ] || fail "Cannot run $ISABELLE_TOOL"

   106 if [ "$1" = "-l" ]; then

   107   shift

   108   [ "$#" -lt "3" ] && usage

   109   LOGIC="$1"

   110   TARGETS="$2"

   111   shift 2

   112   ISABELLE_HOME="$($ISABELLE_TOOL getenv -b ISABELLE_HOME)"

   113   DIR="$ISABELLE_HOME/src/$LOGIC"

   114   TOOL="$ISABELLE_TOOL make $MFLAGS $TARGETS"

   115 else

   116   DIR="."

   117   TOOL="$ISABELLE_TOOL makeall $MFLAGS all"

   118 fi

   120 IDENT=$(cat "$DISTPREFIX/ISABELLE_IDENT")

   122 # main test loop

   124 log "starting [$@]"

   126 for SETTINGS in $@; do

   128     [ -r $SETTINGS ] || fail "Cannot read $SETTINGS."

   130     # logfile setup

   132     DATE=$(date "+%Y-%m-%d")

   133     SHORT=${SETTINGS##*/}

   135 	if [ "${SHORT%-e}" == "$SHORT" ]; then

   136 		# normal test

   137     	TESTLOG=$LOGPREFIX/isatest-makeall-$SHORT-$DATE-$HOSTNAME.log

   138  	else

   139 	 	# experimental test

   140 		TESTLOG=$LOGPREFIX/isatest-makeall-$SHORT-$DATE-$HOSTNAME-e.log

   141 	fi

   143     # the test

   145     touch $RUNNING/$SHORT.running

   147     echo ------------------- starting test --- `date` --- $HOSTNAME > $TESTLOG 2>&1

   149     echo "Isabelle version: $IDENT" >> $TESTLOG 2>&1

   151     if [ "${ISABELLE_HOME_USER:0:14}" == "/tmp/isabelle-" ]; then

   152         echo "--- cleaning up old $ISABELLE_HOME_USER"

   153         rm -rf $ISABELLE_HOME_USER

   154     fi

   156     cp $DISTPREFIX/Isabelle/etc/settings.orig $DISTPREFIX/Isabelle/etc/settings

   157     cat $SETTINGS >> $DISTPREFIX/Isabelle/etc/settings

   158     (ulimit -t $MAXTIME; cd $DIR; $NICE $TOOL >> $TESTLOG 2>&1)

   160     if [ $? -eq 0 ]

   161     then

   162         # test log and cleanup

   163         echo ------------------- test successful --- `date` --- $HOSTNAME >> $TESTLOG 2>&1

   164         if [ -x $PUBLISH_TEST ]; then

   165             $PUBLISH_TEST -r $IDENT -s "SUCCESS" -a log $TESTLOG -n Makeall_isatest_$SHORT

   166         fi

   167         gzip -f $TESTLOG

   168     else

   169         # test log

   170         echo ------------------- test FAILED --- `date` --- $HOSTNAME >> $TESTLOG 2>&1

   171         if [ -x $PUBLISH_TEST ]; then

   172              $PUBLISH_TEST -r $IDENT -s "FAIL" -a log $TESTLOG -n Makeall_isatest_$SHORT

   173         fi

   175         # error log

   176         echo "Test for platform ${SHORT} failed. Log file attached." >> $ERRORLOG

   177         echo "[...]" >> $ERRORLOG

   178         tail -3 $TESTLOG >> $ERRORLOG

   179         echo >> $ERRORLOG

   181         FAIL="$FAIL$SHORT "

   182         (cd $ERRORDIR; cp $TESTLOG .)

   183     fi

   185     rm -f $RUNNING/$SHORT.running

   186 done

   188 # time and success/failure to master log

   189 ELAPSED=$("$HOME/bin/showtime" "$SECONDS")

   191 if [ -z "$FAIL" ]; then

   192     log "all tests successful, elapsed time $ELAPSED."

   193 else

   194     log "targets ${FAIL}FAILED, elapsed time $ELAPSED."

   195     exit 1

   196 fi

   198 # end

author	wenzelm
	Thu, 07 Jul 2011 23:55:15 +0200
changeset 44572	91c4d7397f0e
parent 42838	6aa69999da8f
child 45849	a04f3eb3943c
permissions	-rwxr-xr-x