Admin/isatest/isatest-makeall
author wenzelm
Sun, 20 Jan 2013 13:59:13 +0100
changeset 50990 11996ea98bbe
parent 50149 aaf276a28551
child 58423 e4d540c0dd57
permissions -rwxr-xr-x
tuned;
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
# Author: Gerwin Klein, TU Muenchen
da313b67a04d moved all isatest/cron job related files to own directory
kleing
parents:
diff changeset
     4
#
48608
88ff12baccba updated isatest to isabelle build, which also includes doc-src sessions;
wenzelm
parents: 48259
diff changeset
     5
# DESCRIPTION: Run isabelle build from specified distribution and settings.
22410
da313b67a04d moved all isatest/cron job related files to own directory
kleing
parents:
diff changeset
     6
da313b67a04d moved all isatest/cron job related files to own directory
kleing
parents:
diff changeset
     7
## global settings
22411
1956d895a4ed adjust paths
kleing
parents: 22410
diff changeset
     8
. ~/admin/isatest/isatest-settings
22410
da313b67a04d moved all isatest/cron job related files to own directory
kleing
parents:
diff changeset
     9
da313b67a04d moved all isatest/cron job related files to own directory
kleing
parents:
diff changeset
    10
# max time until test is aborted (in sec)
da313b67a04d moved all isatest/cron job related files to own directory
kleing
parents:
diff changeset
    11
MAXTIME=28800
da313b67a04d moved all isatest/cron job related files to own directory
kleing
parents:
diff changeset
    12
48259
1635298d8fe7 removed some old/unused stuff;
wenzelm
parents: 48258
diff changeset
    13
22410
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
48608
88ff12baccba updated isatest to isabelle build, which also includes doc-src sessions;
wenzelm
parents: 48259
diff changeset
    21
  echo "Usage: $PRG [-l targets] settings1 [settings2 ...]"
22410
da313b67a04d moved all isatest/cron job related files to own directory
kleing
parents:
diff changeset
    22
  echo
48608
88ff12baccba updated isatest to isabelle build, which also includes doc-src sessions;
wenzelm
parents: 48259
diff changeset
    23
  echo "  Runs isabelle build 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"
48608
88ff12baccba updated isatest to isabelle build, which also includes doc-src sessions;
wenzelm
parents: 48259
diff changeset
    28
  echo "  $PRG -l \"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
48259
1635298d8fe7 removed some old/unused stuff;
wenzelm
parents: 48258
diff changeset
    39
22410
da313b67a04d moved all isatest/cron job related files to own directory
kleing
parents:
diff changeset
    40
## main
da313b67a04d moved all isatest/cron job related files to own directory
kleing
parents:
diff changeset
    41
da313b67a04d moved all isatest/cron job related files to own directory
kleing
parents:
diff changeset
    42
# argument checking
da313b67a04d moved all isatest/cron job related files to own directory
kleing
parents:
diff changeset
    43
da313b67a04d moved all isatest/cron job related files to own directory
kleing
parents:
diff changeset
    44
[ "$1" = "-?" ] && usage
da313b67a04d moved all isatest/cron job related files to own directory
kleing
parents:
diff changeset
    45
[ "$#" -lt "1" ] && usage
da313b67a04d moved all isatest/cron job related files to own directory
kleing
parents:
diff changeset
    46
da313b67a04d moved all isatest/cron job related files to own directory
kleing
parents:
diff changeset
    47
[ -d $DISTPREFIX ] || fail "$DISTPREFIX is not a directory."
da313b67a04d moved all isatest/cron job related files to own directory
kleing
parents:
diff changeset
    48
48608
88ff12baccba updated isatest to isabelle build, which also includes doc-src sessions;
wenzelm
parents: 48259
diff changeset
    49
# build args and nice setup for different target platforms
50149
aaf276a28551 more generous timeout for SML/NJ, which is approx. 40-80 times slower than Poly/ML;
wenzelm
parents: 50129
diff changeset
    50
BUILD_ARGS="-v"
48259
1635298d8fe7 removed some old/unused stuff;
wenzelm
parents: 48258
diff changeset
    51
NICE="nice"
22410
da313b67a04d moved all isatest/cron job related files to own directory
kleing
parents:
diff changeset
    52
case $HOSTNAME in
48259
1635298d8fe7 removed some old/unused stuff;
wenzelm
parents: 48258
diff changeset
    53
    macbroy2 | macbroy6 | macbroy30)
31581
907616b9536c more isatests;
wenzelm
parents: 31496
diff changeset
    54
        NICE=""
907616b9536c more isatests;
wenzelm
parents: 31496
diff changeset
    55
        ;;
48158
68a32e12b999 more tests on lxbroy[234], which are 4 core Xeon machines;
wenzelm
parents: 48147
diff changeset
    56
    lxbroy[234])
48608
88ff12baccba updated isatest to isabelle build, which also includes doc-src sessions;
wenzelm
parents: 48259
diff changeset
    57
        BUILD_ARGS="$BUILD_ARGS -j 2"
48158
68a32e12b999 more tests on lxbroy[234], which are 4 core Xeon machines;
wenzelm
parents: 48147
diff changeset
    58
        NICE=""
68a32e12b999 more tests on lxbroy[234], which are 4 core Xeon machines;
wenzelm
parents: 48147
diff changeset
    59
        ;;
68a32e12b999 more tests on lxbroy[234], which are 4 core Xeon machines;
wenzelm
parents: 48147
diff changeset
    60
22410
da313b67a04d moved all isatest/cron job related files to own directory
kleing
parents:
diff changeset
    61
esac
da313b67a04d moved all isatest/cron job related files to own directory
kleing
parents:
diff changeset
    62
28504
7ad7d7d6df47 simplified main Isabelle executables: removed Isabelle and isabelle (replaced by isabelle-process), renamed isatool to isabelle;
wenzelm
parents: 28500
diff changeset
    63
ISABELLE_TOOL="$DISTPREFIX/Isabelle/bin/isabelle"
48608
88ff12baccba updated isatest to isabelle build, which also includes doc-src sessions;
wenzelm
parents: 48259
diff changeset
    64
[ -x $ISABELLE_TOOL ] || fail "Cannot run $ISABELLE_TOOL"
24753
88e34d7af6e3 accept single logic and target as argument
kleing
parents: 24647
diff changeset
    65
48608
88ff12baccba updated isatest to isabelle build, which also includes doc-src sessions;
wenzelm
parents: 48259
diff changeset
    66
ISABELLE_HOME="$($ISABELLE_TOOL getenv -b ISABELLE_HOME)"
24753
88e34d7af6e3 accept single logic and target as argument
kleing
parents: 24647
diff changeset
    67
88e34d7af6e3 accept single logic and target as argument
kleing
parents: 24647
diff changeset
    68
if [ "$1" = "-l" ]; then
88e34d7af6e3 accept single logic and target as argument
kleing
parents: 24647
diff changeset
    69
  shift
48608
88ff12baccba updated isatest to isabelle build, which also includes doc-src sessions;
wenzelm
parents: 48259
diff changeset
    70
  [ "$#" -lt 2 ] && usage
88ff12baccba updated isatest to isabelle build, which also includes doc-src sessions;
wenzelm
parents: 48259
diff changeset
    71
  BUILD_ARGS="$BUILD_ARGS $1"
88ff12baccba updated isatest to isabelle build, which also includes doc-src sessions;
wenzelm
parents: 48259
diff changeset
    72
  shift
24753
88e34d7af6e3 accept single logic and target as argument
kleing
parents: 24647
diff changeset
    73
else
48608
88ff12baccba updated isatest to isabelle build, which also includes doc-src sessions;
wenzelm
parents: 48259
diff changeset
    74
  BUILD_ARGS="$BUILD_ARGS -a"
24753
88e34d7af6e3 accept single logic and target as argument
kleing
parents: 24647
diff changeset
    75
fi
88e34d7af6e3 accept single logic and target as argument
kleing
parents: 24647
diff changeset
    76
32505
eb82ed858b84 isatest: collect test results and logs in testdata repository
krauss
parents: 32418
diff changeset
    77
IDENT=$(cat "$DISTPREFIX/ISABELLE_IDENT")
eb82ed858b84 isatest: collect test results and logs in testdata repository
krauss
parents: 32418
diff changeset
    78
48259
1635298d8fe7 removed some old/unused stuff;
wenzelm
parents: 48258
diff changeset
    79
22410
da313b67a04d moved all isatest/cron job related files to own directory
kleing
parents:
diff changeset
    80
# main test loop
da313b67a04d moved all isatest/cron job related files to own directory
kleing
parents:
diff changeset
    81
28597
e76e7b96a517 log start of test session
kleing
parents: 28539
diff changeset
    82
log "starting [$@]"
e76e7b96a517 log start of test session
kleing
parents: 28539
diff changeset
    83
22410
da313b67a04d moved all isatest/cron job related files to own directory
kleing
parents:
diff changeset
    84
for SETTINGS in $@; do
da313b67a04d moved all isatest/cron job related files to own directory
kleing
parents:
diff changeset
    85
da313b67a04d moved all isatest/cron job related files to own directory
kleing
parents:
diff changeset
    86
    [ -r $SETTINGS ] || fail "Cannot read $SETTINGS."
da313b67a04d moved all isatest/cron job related files to own directory
kleing
parents:
diff changeset
    87
50149
aaf276a28551 more generous timeout for SML/NJ, which is approx. 40-80 times slower than Poly/ML;
wenzelm
parents: 50129
diff changeset
    88
    case "$SETTINGS" in
aaf276a28551 more generous timeout for SML/NJ, which is approx. 40-80 times slower than Poly/ML;
wenzelm
parents: 50129
diff changeset
    89
      *sml*)
aaf276a28551 more generous timeout for SML/NJ, which is approx. 40-80 times slower than Poly/ML;
wenzelm
parents: 50129
diff changeset
    90
        BUILD_ARGS="-o timeout=36000 $BUILD_ARGS"
aaf276a28551 more generous timeout for SML/NJ, which is approx. 40-80 times slower than Poly/ML;
wenzelm
parents: 50129
diff changeset
    91
        ;;
aaf276a28551 more generous timeout for SML/NJ, which is approx. 40-80 times slower than Poly/ML;
wenzelm
parents: 50129
diff changeset
    92
      *)
aaf276a28551 more generous timeout for SML/NJ, which is approx. 40-80 times slower than Poly/ML;
wenzelm
parents: 50129
diff changeset
    93
        BUILD_ARGS="-o timeout=3600 $BUILD_ARGS"
aaf276a28551 more generous timeout for SML/NJ, which is approx. 40-80 times slower than Poly/ML;
wenzelm
parents: 50129
diff changeset
    94
        ;;
aaf276a28551 more generous timeout for SML/NJ, which is approx. 40-80 times slower than Poly/ML;
wenzelm
parents: 50129
diff changeset
    95
    esac
aaf276a28551 more generous timeout for SML/NJ, which is approx. 40-80 times slower than Poly/ML;
wenzelm
parents: 50129
diff changeset
    96
22410
da313b67a04d moved all isatest/cron job related files to own directory
kleing
parents:
diff changeset
    97
    # logfile setup
da313b67a04d moved all isatest/cron job related files to own directory
kleing
parents:
diff changeset
    98
da313b67a04d moved all isatest/cron job related files to own directory
kleing
parents:
diff changeset
    99
    DATE=$(date "+%Y-%m-%d")
da313b67a04d moved all isatest/cron job related files to own directory
kleing
parents:
diff changeset
   100
    SHORT=${SETTINGS##*/}
28527
82b36daff4c1 make the test for experimental sessions in isatest-check actually work
kleing
parents: 28504
diff changeset
   101
48259
1635298d8fe7 removed some old/unused stuff;
wenzelm
parents: 48258
diff changeset
   102
    if [ "${SHORT%-e}" == "$SHORT" ]; then
1635298d8fe7 removed some old/unused stuff;
wenzelm
parents: 48258
diff changeset
   103
        # normal test
1635298d8fe7 removed some old/unused stuff;
wenzelm
parents: 48258
diff changeset
   104
        TESTLOG=$LOGPREFIX/isatest-makeall-$SHORT-$DATE-$HOSTNAME.log
1635298d8fe7 removed some old/unused stuff;
wenzelm
parents: 48258
diff changeset
   105
    else
1635298d8fe7 removed some old/unused stuff;
wenzelm
parents: 48258
diff changeset
   106
        # experimental test
1635298d8fe7 removed some old/unused stuff;
wenzelm
parents: 48258
diff changeset
   107
        TESTLOG=$LOGPREFIX/isatest-makeall-$SHORT-$DATE-$HOSTNAME-e.log
1635298d8fe7 removed some old/unused stuff;
wenzelm
parents: 48258
diff changeset
   108
    fi
22410
da313b67a04d moved all isatest/cron job related files to own directory
kleing
parents:
diff changeset
   109
da313b67a04d moved all isatest/cron job related files to own directory
kleing
parents:
diff changeset
   110
    # the test
da313b67a04d moved all isatest/cron job related files to own directory
kleing
parents:
diff changeset
   111
da313b67a04d moved all isatest/cron job related files to own directory
kleing
parents:
diff changeset
   112
    touch $RUNNING/$SHORT.running
da313b67a04d moved all isatest/cron job related files to own directory
kleing
parents:
diff changeset
   113
da313b67a04d moved all isatest/cron job related files to own directory
kleing
parents:
diff changeset
   114
    echo ------------------- starting test --- `date` --- $HOSTNAME > $TESTLOG 2>&1
da313b67a04d moved all isatest/cron job related files to own directory
kleing
parents:
diff changeset
   115
39686
8b9f971ace20 isatest: indicate Isabelle version;
wenzelm
parents: 38434
diff changeset
   116
    echo "Isabelle version: $IDENT" >> $TESTLOG 2>&1
8b9f971ace20 isatest: indicate Isabelle version;
wenzelm
parents: 38434
diff changeset
   117
28982
75f221d67515 run test for sunbroy2 on /tmp,
kleing
parents: 28597
diff changeset
   118
    if [ "${ISABELLE_HOME_USER:0:14}" == "/tmp/isabelle-" ]; then
75f221d67515 run test for sunbroy2 on /tmp,
kleing
parents: 28597
diff changeset
   119
        echo "--- cleaning up old $ISABELLE_HOME_USER"
75f221d67515 run test for sunbroy2 on /tmp,
kleing
parents: 28597
diff changeset
   120
        rm -rf $ISABELLE_HOME_USER
75f221d67515 run test for sunbroy2 on /tmp,
kleing
parents: 28597
diff changeset
   121
    fi
75f221d67515 run test for sunbroy2 on /tmp,
kleing
parents: 28597
diff changeset
   122
41967
6aa69999da8f isatest: fresh copy of settings avoids odd cumulative environment;
wenzelm
parents: 39686
diff changeset
   123
    cp $DISTPREFIX/Isabelle/etc/settings.orig $DISTPREFIX/Isabelle/etc/settings
22410
da313b67a04d moved all isatest/cron job related files to own directory
kleing
parents:
diff changeset
   124
    cat $SETTINGS >> $DISTPREFIX/Isabelle/etc/settings
48608
88ff12baccba updated isatest to isabelle build, which also includes doc-src sessions;
wenzelm
parents: 48259
diff changeset
   125
    (ulimit -t $MAXTIME; $NICE "$ISABELLE_TOOL" build $BUILD_ARGS >> $TESTLOG 2>&1)
22410
da313b67a04d moved all isatest/cron job related files to own directory
kleing
parents:
diff changeset
   126
da313b67a04d moved all isatest/cron job related files to own directory
kleing
parents:
diff changeset
   127
    if [ $? -eq 0 ]
da313b67a04d moved all isatest/cron job related files to own directory
kleing
parents:
diff changeset
   128
    then
da313b67a04d moved all isatest/cron job related files to own directory
kleing
parents:
diff changeset
   129
        # test log and cleanup
da313b67a04d moved all isatest/cron job related files to own directory
kleing
parents:
diff changeset
   130
        echo ------------------- test successful --- `date` --- $HOSTNAME >> $TESTLOG 2>&1
da313b67a04d moved all isatest/cron job related files to own directory
kleing
parents:
diff changeset
   131
        gzip -f $TESTLOG
da313b67a04d moved all isatest/cron job related files to own directory
kleing
parents:
diff changeset
   132
    else
da313b67a04d moved all isatest/cron job related files to own directory
kleing
parents:
diff changeset
   133
        # test log
da313b67a04d moved all isatest/cron job related files to own directory
kleing
parents:
diff changeset
   134
        echo ------------------- test FAILED --- `date` --- $HOSTNAME >> $TESTLOG 2>&1
da313b67a04d moved all isatest/cron job related files to own directory
kleing
parents:
diff changeset
   135
da313b67a04d moved all isatest/cron job related files to own directory
kleing
parents:
diff changeset
   136
        # error log
da313b67a04d moved all isatest/cron job related files to own directory
kleing
parents:
diff changeset
   137
        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
   138
        echo "[...]" >> $ERRORLOG
49978
c163145dd40f longer log, to accomodate final status line of isabelle build;
wenzelm
parents: 48608
diff changeset
   139
        tail -4 $TESTLOG >> $ERRORLOG
22410
da313b67a04d moved all isatest/cron job related files to own directory
kleing
parents:
diff changeset
   140
        echo >> $ERRORLOG
da313b67a04d moved all isatest/cron job related files to own directory
kleing
parents:
diff changeset
   141
da313b67a04d moved all isatest/cron job related files to own directory
kleing
parents:
diff changeset
   142
        FAIL="$FAIL$SHORT "
38434
7aa0245aeede removed non-BSD compatible option from cp
kleing
parents: 37874
diff changeset
   143
        (cd $ERRORDIR; cp $TESTLOG .)
22410
da313b67a04d moved all isatest/cron job related files to own directory
kleing
parents:
diff changeset
   144
    fi
da313b67a04d moved all isatest/cron job related files to own directory
kleing
parents:
diff changeset
   145
da313b67a04d moved all isatest/cron job related files to own directory
kleing
parents:
diff changeset
   146
    rm -f $RUNNING/$SHORT.running
da313b67a04d moved all isatest/cron job related files to own directory
kleing
parents:
diff changeset
   147
done
da313b67a04d moved all isatest/cron job related files to own directory
kleing
parents:
diff changeset
   148
da313b67a04d moved all isatest/cron job related files to own directory
kleing
parents:
diff changeset
   149
# time and success/failure to master log
da313b67a04d moved all isatest/cron job related files to own directory
kleing
parents:
diff changeset
   150
ELAPSED=$("$HOME/bin/showtime" "$SECONDS")
da313b67a04d moved all isatest/cron job related files to own directory
kleing
parents:
diff changeset
   151
da313b67a04d moved all isatest/cron job related files to own directory
kleing
parents:
diff changeset
   152
if [ -z "$FAIL" ]; then
28539
bdb308737bfd do logging to MASTERLOG centrally (avoid multiple writers over NFS as
kleing
parents: 28527
diff changeset
   153
    log "all tests successful, elapsed time $ELAPSED."
22410
da313b67a04d moved all isatest/cron job related files to own directory
kleing
parents:
diff changeset
   154
else
28539
bdb308737bfd do logging to MASTERLOG centrally (avoid multiple writers over NFS as
kleing
parents: 28527
diff changeset
   155
    log "targets ${FAIL}FAILED, elapsed time $ELAPSED."
22410
da313b67a04d moved all isatest/cron job related files to own directory
kleing
parents:
diff changeset
   156
    exit 1
da313b67a04d moved all isatest/cron job related files to own directory
kleing
parents:
diff changeset
   157
fi
da313b67a04d moved all isatest/cron job related files to own directory
kleing
parents:
diff changeset
   158