Admin/isatest/isatest-makeall
author nipkow
Sun, 22 Feb 2009 17:25:28 +0100
changeset 30056 0a35bee25c20
parent 28982 75f221d67515
child 31496 c4b74075fc17
permissions -rwxr-xr-x
added lemmas
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
22410
da313b67a04d moved all isatest/cron job related files to own directory
kleing
parents:
diff changeset
     1
#!/usr/bin/env bash
da313b67a04d moved all isatest/cron job related files to own directory
kleing
parents:
diff changeset
     2
#
da313b67a04d moved all isatest/cron job related files to own directory
kleing
parents:
diff changeset
     3
# $Id$
da313b67a04d moved all isatest/cron job related files to own directory
kleing
parents:
diff changeset
     4
# Author: Gerwin Klein, TU Muenchen
da313b67a04d moved all isatest/cron job related files to own directory
kleing
parents:
diff changeset
     5
#
28504
7ad7d7d6df47 simplified main Isabelle executables: removed Isabelle and isabelle (replaced by isabelle-process), renamed isatool to isabelle;
wenzelm
parents: 28500
diff changeset
     6
# DESCRIPTION: Run isabelle makeall from specified distribution and settings.
22410
da313b67a04d moved all isatest/cron job related files to own directory
kleing
parents:
diff changeset
     7
da313b67a04d moved all isatest/cron job related files to own directory
kleing
parents:
diff changeset
     8
## global settings
22411
1956d895a4ed adjust paths
kleing
parents: 22410
diff changeset
     9
. ~/admin/isatest/isatest-settings
22410
da313b67a04d moved all isatest/cron job related files to own directory
kleing
parents:
diff changeset
    10
da313b67a04d moved all isatest/cron job related files to own directory
kleing
parents:
diff changeset
    11
# max time until test is aborted (in sec)
da313b67a04d moved all isatest/cron job related files to own directory
kleing
parents:
diff changeset
    12
MAXTIME=28800
da313b67a04d moved all isatest/cron job related files to own directory
kleing
parents:
diff changeset
    13
da313b67a04d moved all isatest/cron job related files to own directory
kleing
parents:
diff changeset
    14
## diagnostics
da313b67a04d moved all isatest/cron job related files to own directory
kleing
parents:
diff changeset
    15
da313b67a04d moved all isatest/cron job related files to own directory
kleing
parents:
diff changeset
    16
PRG="$(basename "$0")"
da313b67a04d moved all isatest/cron job related files to own directory
kleing
parents:
diff changeset
    17
da313b67a04d moved all isatest/cron job related files to own directory
kleing
parents:
diff changeset
    18
function usage()
da313b67a04d moved all isatest/cron job related files to own directory
kleing
parents:
diff changeset
    19
{
da313b67a04d moved all isatest/cron job related files to own directory
kleing
parents:
diff changeset
    20
  echo
24753
88e34d7af6e3 accept single logic and target as argument
kleing
parents: 24647
diff changeset
    21
  echo "Usage: $PRG [-l logic targets] settings1 [settings2 ...]"
22410
da313b67a04d moved all isatest/cron job related files to own directory
kleing
parents:
diff changeset
    22
  echo
28504
7ad7d7d6df47 simplified main Isabelle executables: removed Isabelle and isabelle (replaced by isabelle-process), renamed isatool to isabelle;
wenzelm
parents: 28500
diff changeset
    23
  echo "  Runs isabelle makeall for specified settings."
22410
da313b67a04d moved all isatest/cron job related files to own directory
kleing
parents:
diff changeset
    24
  echo "  Leaves messages in ${ERRORLOG} and ${LOGPREFIX} if it fails."
da313b67a04d moved all isatest/cron job related files to own directory
kleing
parents:
diff changeset
    25
  echo
24753
88e34d7af6e3 accept single logic and target as argument
kleing
parents: 24647
diff changeset
    26
  echo "Examples:"
88e34d7af6e3 accept single logic and target as argument
kleing
parents: 24647
diff changeset
    27
  echo "  $PRG ~/settings/at-poly ~/settings/at-sml"
88e34d7af6e3 accept single logic and target as argument
kleing
parents: 24647
diff changeset
    28
  echo "  $PRG -l HOL \"HOL-Library HOL-Bali\" ~/settings/at-poly"
22410
da313b67a04d moved all isatest/cron job related files to own directory
kleing
parents:
diff changeset
    29
  exit 1
da313b67a04d moved all isatest/cron job related files to own directory
kleing
parents:
diff changeset
    30
}
da313b67a04d moved all isatest/cron job related files to own directory
kleing
parents:
diff changeset
    31
da313b67a04d moved all isatest/cron job related files to own directory
kleing
parents:
diff changeset
    32
function fail()
da313b67a04d moved all isatest/cron job related files to own directory
kleing
parents:
diff changeset
    33
{
da313b67a04d moved all isatest/cron job related files to own directory
kleing
parents:
diff changeset
    34
  echo "$1" >&2
28539
bdb308737bfd do logging to MASTERLOG centrally (avoid multiple writers over NFS as
kleing
parents: 28527
diff changeset
    35
  log "FAILED, $1"
22410
da313b67a04d moved all isatest/cron job related files to own directory
kleing
parents:
diff changeset
    36
  exit 2
da313b67a04d moved all isatest/cron job related files to own directory
kleing
parents:
diff changeset
    37
}
da313b67a04d moved all isatest/cron job related files to own directory
kleing
parents:
diff changeset
    38
da313b67a04d moved all isatest/cron job related files to own directory
kleing
parents:
diff changeset
    39
## main
da313b67a04d moved all isatest/cron job related files to own directory
kleing
parents:
diff changeset
    40
da313b67a04d moved all isatest/cron job related files to own directory
kleing
parents:
diff changeset
    41
# argument checking
da313b67a04d moved all isatest/cron job related files to own directory
kleing
parents:
diff changeset
    42
da313b67a04d moved all isatest/cron job related files to own directory
kleing
parents:
diff changeset
    43
[ "$1" = "-?" ] && usage
da313b67a04d moved all isatest/cron job related files to own directory
kleing
parents:
diff changeset
    44
[ "$#" -lt "1" ] && usage
da313b67a04d moved all isatest/cron job related files to own directory
kleing
parents:
diff changeset
    45
da313b67a04d moved all isatest/cron job related files to own directory
kleing
parents:
diff changeset
    46
[ -d $DISTPREFIX ] || fail "$DISTPREFIX is not a directory."
da313b67a04d moved all isatest/cron job related files to own directory
kleing
parents:
diff changeset
    47
da313b67a04d moved all isatest/cron job related files to own directory
kleing
parents:
diff changeset
    48
# make file flags and nice setup for different target platforms
da313b67a04d moved all isatest/cron job related files to own directory
kleing
parents:
diff changeset
    49
case $HOSTNAME in
da313b67a04d moved all isatest/cron job related files to own directory
kleing
parents:
diff changeset
    50
    atbroy51)
da313b67a04d moved all isatest/cron job related files to own directory
kleing
parents:
diff changeset
    51
        MFLAGS="-j 2"
da313b67a04d moved all isatest/cron job related files to own directory
kleing
parents:
diff changeset
    52
        NICE=""
da313b67a04d moved all isatest/cron job related files to own directory
kleing
parents:
diff changeset
    53
        ;;
da313b67a04d moved all isatest/cron job related files to own directory
kleing
parents:
diff changeset
    54
24758
53c1a0a46db3 swapped machines for at-sml-dev and at-sml-dev-p
isatest
parents: 24753
diff changeset
    55
    atbroy98)
26369
01ee1168088b tuned settings for target platforms;
wenzelm
parents: 25912
diff changeset
    56
        MFLAGS=""
01ee1168088b tuned settings for target platforms;
wenzelm
parents: 25912
diff changeset
    57
        NICE=""
01ee1168088b tuned settings for target platforms;
wenzelm
parents: 25912
diff changeset
    58
        ;;
24647
212c9b342a67 move at-sml-dev to 2-processor atbroy100
isatest
parents: 23415
diff changeset
    59
22410
da313b67a04d moved all isatest/cron job related files to own directory
kleing
parents:
diff changeset
    60
    atbroy31)
26369
01ee1168088b tuned settings for target platforms;
wenzelm
parents: 25912
diff changeset
    61
        MFLAGS="-j 2"
22410
da313b67a04d moved all isatest/cron job related files to own directory
kleing
parents:
diff changeset
    62
        ;;
da313b67a04d moved all isatest/cron job related files to own directory
kleing
parents:
diff changeset
    63
  
da313b67a04d moved all isatest/cron job related files to own directory
kleing
parents:
diff changeset
    64
    sunbroy2)
da313b67a04d moved all isatest/cron job related files to own directory
kleing
parents:
diff changeset
    65
        MFLAGS="-j 6"
da313b67a04d moved all isatest/cron job related files to own directory
kleing
parents:
diff changeset
    66
        NICE="nice"
da313b67a04d moved all isatest/cron job related files to own directory
kleing
parents:
diff changeset
    67
        ;;
da313b67a04d moved all isatest/cron job related files to own directory
kleing
parents:
diff changeset
    68
da313b67a04d moved all isatest/cron job related files to own directory
kleing
parents:
diff changeset
    69
    sunbroy1)
da313b67a04d moved all isatest/cron job related files to own directory
kleing
parents:
diff changeset
    70
        MFLAGS="-j 2"
da313b67a04d moved all isatest/cron job related files to own directory
kleing
parents:
diff changeset
    71
        NICE="nice"
da313b67a04d moved all isatest/cron job related files to own directory
kleing
parents:
diff changeset
    72
        ;;
da313b67a04d moved all isatest/cron job related files to own directory
kleing
parents:
diff changeset
    73
da313b67a04d moved all isatest/cron job related files to own directory
kleing
parents:
diff changeset
    74
    macbroy5)
23415
9dad8095bd43 macbroy5: trying -j 2;
wenzelm
parents: 22411
diff changeset
    75
        MFLAGS="-j 2"
22410
da313b67a04d moved all isatest/cron job related files to own directory
kleing
parents:
diff changeset
    76
        NICE=""
da313b67a04d moved all isatest/cron job related files to own directory
kleing
parents:
diff changeset
    77
        ;;
da313b67a04d moved all isatest/cron job related files to own directory
kleing
parents:
diff changeset
    78
26369
01ee1168088b tuned settings for target platforms;
wenzelm
parents: 25912
diff changeset
    79
    macbroy2[0-9])
01ee1168088b tuned settings for target platforms;
wenzelm
parents: 25912
diff changeset
    80
        MFLAGS="-j 2"
01ee1168088b tuned settings for target platforms;
wenzelm
parents: 25912
diff changeset
    81
        NICE=""
01ee1168088b tuned settings for target platforms;
wenzelm
parents: 25912
diff changeset
    82
        ;;
01ee1168088b tuned settings for target platforms;
wenzelm
parents: 25912
diff changeset
    83
22410
da313b67a04d moved all isatest/cron job related files to own directory
kleing
parents:
diff changeset
    84
    *)
da313b67a04d moved all isatest/cron job related files to own directory
kleing
parents:
diff changeset
    85
        MFLAGS=""
da313b67a04d moved all isatest/cron job related files to own directory
kleing
parents:
diff changeset
    86
        # be nice by default
da313b67a04d moved all isatest/cron job related files to own directory
kleing
parents:
diff changeset
    87
        NICE=nice
da313b67a04d moved all isatest/cron job related files to own directory
kleing
parents:
diff changeset
    88
        ;;
da313b67a04d moved all isatest/cron job related files to own directory
kleing
parents:
diff changeset
    89
esac
da313b67a04d moved all isatest/cron job related files to own directory
kleing
parents:
diff changeset
    90
28504
7ad7d7d6df47 simplified main Isabelle executables: removed Isabelle and isabelle (replaced by isabelle-process), renamed isatool to isabelle;
wenzelm
parents: 28500
diff changeset
    91
ISABELLE_TOOL="$DISTPREFIX/Isabelle/bin/isabelle"
24753
88e34d7af6e3 accept single logic and target as argument
kleing
parents: 24647
diff changeset
    92
28500
4b79e5d3d0aa replaced ISATOOL by ISABELLE_TOOL;
wenzelm
parents: 26369
diff changeset
    93
[ -x $ISABELLE_TOOL ] || fail "Cannot run $ISABELLE_TOOL"
24753
88e34d7af6e3 accept single logic and target as argument
kleing
parents: 24647
diff changeset
    94
88e34d7af6e3 accept single logic and target as argument
kleing
parents: 24647
diff changeset
    95
if [ "$1" = "-l" ]; then
88e34d7af6e3 accept single logic and target as argument
kleing
parents: 24647
diff changeset
    96
  shift
88e34d7af6e3 accept single logic and target as argument
kleing
parents: 24647
diff changeset
    97
  [ "$#" -lt "3" ] && usage
88e34d7af6e3 accept single logic and target as argument
kleing
parents: 24647
diff changeset
    98
  LOGIC="$1"
88e34d7af6e3 accept single logic and target as argument
kleing
parents: 24647
diff changeset
    99
  TARGETS="$2"
88e34d7af6e3 accept single logic and target as argument
kleing
parents: 24647
diff changeset
   100
  shift 2
28500
4b79e5d3d0aa replaced ISATOOL by ISABELLE_TOOL;
wenzelm
parents: 26369
diff changeset
   101
  ISABELLE_HOME="$($ISABELLE_TOOL getenv -b ISABELLE_HOME)"
24786
56b8b2cfa08e fixed dir in single-logic test
isatest
parents: 24781
diff changeset
   102
  DIR="$ISABELLE_HOME/src/$LOGIC"
28500
4b79e5d3d0aa replaced ISATOOL by ISABELLE_TOOL;
wenzelm
parents: 26369
diff changeset
   103
  TOOL="$ISABELLE_TOOL make $MFLAGS $TARGETS"
24753
88e34d7af6e3 accept single logic and target as argument
kleing
parents: 24647
diff changeset
   104
else
24781
fd6d2040f89b fix shell quoting confusion
isatest
parents: 24758
diff changeset
   105
  DIR="."
28500
4b79e5d3d0aa replaced ISATOOL by ISABELLE_TOOL;
wenzelm
parents: 26369
diff changeset
   106
  TOOL="$ISABELLE_TOOL makeall $MFLAGS all"
24753
88e34d7af6e3 accept single logic and target as argument
kleing
parents: 24647
diff changeset
   107
fi
88e34d7af6e3 accept single logic and target as argument
kleing
parents: 24647
diff changeset
   108
22410
da313b67a04d moved all isatest/cron job related files to own directory
kleing
parents:
diff changeset
   109
# main test loop
da313b67a04d moved all isatest/cron job related files to own directory
kleing
parents:
diff changeset
   110
28597
e76e7b96a517 log start of test session
kleing
parents: 28539
diff changeset
   111
log "starting [$@]"
e76e7b96a517 log start of test session
kleing
parents: 28539
diff changeset
   112
22410
da313b67a04d moved all isatest/cron job related files to own directory
kleing
parents:
diff changeset
   113
for SETTINGS in $@; do
da313b67a04d moved all isatest/cron job related files to own directory
kleing
parents:
diff changeset
   114
da313b67a04d moved all isatest/cron job related files to own directory
kleing
parents:
diff changeset
   115
    [ -r $SETTINGS ] || fail "Cannot read $SETTINGS."
da313b67a04d moved all isatest/cron job related files to own directory
kleing
parents:
diff changeset
   116
da313b67a04d moved all isatest/cron job related files to own directory
kleing
parents:
diff changeset
   117
    # logfile setup
da313b67a04d moved all isatest/cron job related files to own directory
kleing
parents:
diff changeset
   118
da313b67a04d moved all isatest/cron job related files to own directory
kleing
parents:
diff changeset
   119
    DATE=$(date "+%Y-%m-%d")
da313b67a04d moved all isatest/cron job related files to own directory
kleing
parents:
diff changeset
   120
    SHORT=${SETTINGS##*/}
28527
82b36daff4c1 make the test for experimental sessions in isatest-check actually work
kleing
parents: 28504
diff changeset
   121
82b36daff4c1 make the test for experimental sessions in isatest-check actually work
kleing
parents: 28504
diff changeset
   122
	if [ "${SHORT%-e}" == "$SHORT" ]; then
82b36daff4c1 make the test for experimental sessions in isatest-check actually work
kleing
parents: 28504
diff changeset
   123
		# normal test
82b36daff4c1 make the test for experimental sessions in isatest-check actually work
kleing
parents: 28504
diff changeset
   124
    	TESTLOG=$LOGPREFIX/isatest-makeall-$SHORT-$DATE-$HOSTNAME.log
82b36daff4c1 make the test for experimental sessions in isatest-check actually work
kleing
parents: 28504
diff changeset
   125
 	else
82b36daff4c1 make the test for experimental sessions in isatest-check actually work
kleing
parents: 28504
diff changeset
   126
	 	# experimental test
82b36daff4c1 make the test for experimental sessions in isatest-check actually work
kleing
parents: 28504
diff changeset
   127
		TESTLOG=$LOGPREFIX/isatest-makeall-$SHORT-$DATE-$HOSTNAME-e.log
82b36daff4c1 make the test for experimental sessions in isatest-check actually work
kleing
parents: 28504
diff changeset
   128
	fi
22410
da313b67a04d moved all isatest/cron job related files to own directory
kleing
parents:
diff changeset
   129
da313b67a04d moved all isatest/cron job related files to own directory
kleing
parents:
diff changeset
   130
    # the test
da313b67a04d moved all isatest/cron job related files to own directory
kleing
parents:
diff changeset
   131
da313b67a04d moved all isatest/cron job related files to own directory
kleing
parents:
diff changeset
   132
    touch $RUNNING/$SHORT.running
da313b67a04d moved all isatest/cron job related files to own directory
kleing
parents:
diff changeset
   133
da313b67a04d moved all isatest/cron job related files to own directory
kleing
parents:
diff changeset
   134
    echo ------------------- starting test --- `date` --- $HOSTNAME > $TESTLOG 2>&1
da313b67a04d moved all isatest/cron job related files to own directory
kleing
parents:
diff changeset
   135
28982
75f221d67515 run test for sunbroy2 on /tmp,
kleing
parents: 28597
diff changeset
   136
    if [ "${ISABELLE_HOME_USER:0:14}" == "/tmp/isabelle-" ]; then
75f221d67515 run test for sunbroy2 on /tmp,
kleing
parents: 28597
diff changeset
   137
        echo "--- cleaning up old $ISABELLE_HOME_USER"
75f221d67515 run test for sunbroy2 on /tmp,
kleing
parents: 28597
diff changeset
   138
        rm -rf $ISABELLE_HOME_USER
75f221d67515 run test for sunbroy2 on /tmp,
kleing
parents: 28597
diff changeset
   139
    fi
75f221d67515 run test for sunbroy2 on /tmp,
kleing
parents: 28597
diff changeset
   140
22410
da313b67a04d moved all isatest/cron job related files to own directory
kleing
parents:
diff changeset
   141
    cat $SETTINGS >> $DISTPREFIX/Isabelle/etc/settings
24781
fd6d2040f89b fix shell quoting confusion
isatest
parents: 24758
diff changeset
   142
    (ulimit -t $MAXTIME; cd $DIR; $NICE $TOOL >> $TESTLOG 2>&1)
22410
da313b67a04d moved all isatest/cron job related files to own directory
kleing
parents:
diff changeset
   143
da313b67a04d moved all isatest/cron job related files to own directory
kleing
parents:
diff changeset
   144
    if [ $? -eq 0 ]
da313b67a04d moved all isatest/cron job related files to own directory
kleing
parents:
diff changeset
   145
    then
da313b67a04d moved all isatest/cron job related files to own directory
kleing
parents:
diff changeset
   146
        # test log and cleanup
da313b67a04d moved all isatest/cron job related files to own directory
kleing
parents:
diff changeset
   147
        echo ------------------- test successful --- `date` --- $HOSTNAME >> $TESTLOG 2>&1
da313b67a04d moved all isatest/cron job related files to own directory
kleing
parents:
diff changeset
   148
        gzip -f $TESTLOG
da313b67a04d moved all isatest/cron job related files to own directory
kleing
parents:
diff changeset
   149
    else
da313b67a04d moved all isatest/cron job related files to own directory
kleing
parents:
diff changeset
   150
        # test log
da313b67a04d moved all isatest/cron job related files to own directory
kleing
parents:
diff changeset
   151
        echo ------------------- test FAILED --- `date` --- $HOSTNAME >> $TESTLOG 2>&1
da313b67a04d moved all isatest/cron job related files to own directory
kleing
parents:
diff changeset
   152
da313b67a04d moved all isatest/cron job related files to own directory
kleing
parents:
diff changeset
   153
        # error log
da313b67a04d moved all isatest/cron job related files to own directory
kleing
parents:
diff changeset
   154
        echo "Test for platform ${SHORT} failed. Log file attached." >> $ERRORLOG
da313b67a04d moved all isatest/cron job related files to own directory
kleing
parents:
diff changeset
   155
        echo "[...]" >> $ERRORLOG
da313b67a04d moved all isatest/cron job related files to own directory
kleing
parents:
diff changeset
   156
        tail -3 $TESTLOG >> $ERRORLOG
da313b67a04d moved all isatest/cron job related files to own directory
kleing
parents:
diff changeset
   157
        echo >> $ERRORLOG
da313b67a04d moved all isatest/cron job related files to own directory
kleing
parents:
diff changeset
   158
da313b67a04d moved all isatest/cron job related files to own directory
kleing
parents:
diff changeset
   159
        FAIL="$FAIL$SHORT "
da313b67a04d moved all isatest/cron job related files to own directory
kleing
parents:
diff changeset
   160
        (cd $ERRORDIR; ln -s $TESTLOG)
da313b67a04d moved all isatest/cron job related files to own directory
kleing
parents:
diff changeset
   161
    fi
da313b67a04d moved all isatest/cron job related files to own directory
kleing
parents:
diff changeset
   162
da313b67a04d moved all isatest/cron job related files to own directory
kleing
parents:
diff changeset
   163
    rm -f $RUNNING/$SHORT.running
da313b67a04d moved all isatest/cron job related files to own directory
kleing
parents:
diff changeset
   164
done
da313b67a04d moved all isatest/cron job related files to own directory
kleing
parents:
diff changeset
   165
da313b67a04d moved all isatest/cron job related files to own directory
kleing
parents:
diff changeset
   166
# time and success/failure to master log
da313b67a04d moved all isatest/cron job related files to own directory
kleing
parents:
diff changeset
   167
ELAPSED=$("$HOME/bin/showtime" "$SECONDS")
da313b67a04d moved all isatest/cron job related files to own directory
kleing
parents:
diff changeset
   168
da313b67a04d moved all isatest/cron job related files to own directory
kleing
parents:
diff changeset
   169
if [ -z "$FAIL" ]; then
28539
bdb308737bfd do logging to MASTERLOG centrally (avoid multiple writers over NFS as
kleing
parents: 28527
diff changeset
   170
    log "all tests successful, elapsed time $ELAPSED."
22410
da313b67a04d moved all isatest/cron job related files to own directory
kleing
parents:
diff changeset
   171
else
28539
bdb308737bfd do logging to MASTERLOG centrally (avoid multiple writers over NFS as
kleing
parents: 28527
diff changeset
   172
    log "targets ${FAIL}FAILED, elapsed time $ELAPSED."
22410
da313b67a04d moved all isatest/cron job related files to own directory
kleing
parents:
diff changeset
   173
    exit 1
da313b67a04d moved all isatest/cron job related files to own directory
kleing
parents:
diff changeset
   174
fi
da313b67a04d moved all isatest/cron job related files to own directory
kleing
parents:
diff changeset
   175
da313b67a04d moved all isatest/cron job related files to own directory
kleing
parents:
diff changeset
   176
# end