# HG changeset patch
# User wenzelm
# Date 1343659221 -7200
# Node ID 88ff12baccbae3d3d9a7c43ccdd1e6a34a989379
# Parent  e24bfa4e3b84436b704ce624feeccbbffb3d2c4b
updated isatest to isabelle build, which also includes doc-src sessions;

diff -r e24bfa4e3b84 -r 88ff12baccba Admin/Release/CHECKLIST
--- a/Admin/Release/CHECKLIST	Mon Jul 30 16:03:25 2012 +0200
+++ b/Admin/Release/CHECKLIST	Mon Jul 30 16:40:21 2012 +0200
@@ -26,7 +26,6 @@
 - update https://isabelle.in.tum.de/repos/website;
 
 - maintain Docs:
-    doc-src: make all
     doc-src/Dirs
     doc/Contents
 
diff -r e24bfa4e3b84 -r 88ff12baccba Admin/isatest/crontab.lxbroy2
--- a/Admin/isatest/crontab.lxbroy2	Mon Jul 30 16:03:25 2012 +0200
+++ b/Admin/isatest/crontab.lxbroy2	Mon Jul 30 16:40:21 2012 +0200
@@ -1,7 +1,6 @@
 03 00 * * *                  $HOME/bin/checkout-admin
 17 00 * * *                  $HOME/bin/isatest-makedist
 01 08 * * *                  $HOME/bin/isatest-check
-17 08 * * *                  $HOME/bin/isatest-doc
 
 04 23 31 1,3,5,7,8,10,12 *   $HOME/bin/logmove
 04 23 30 4,6,9,11 *          $HOME/bin/logmove
diff -r e24bfa4e3b84 -r 88ff12baccba Admin/isatest/isatest-doc
--- a/Admin/isatest/isatest-doc	Mon Jul 30 16:03:25 2012 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,120 +0,0 @@
-#!/usr/bin/env bash
-#
-# Author: Gerwin Klein, NICTA
-#
-# Run IsaMakefile for every Doc/ subdirectory.
-#
-# Relies on being run in the isatest environment on sunbroy2.
-# 
-
-. ~/.bashrc
-
-## global settings
-. ~/admin/isatest/isatest-settings
-
-DOCDIR=$HOME/Doc
-
-MAXTIME=1800
-
-ISABELLE_DEVEL=$DISTPREFIX/Isabelle
-DATE=$(date "+%Y-%m-%d")
-
-LOG=$LOGPREFIX/isatest-doc-$DATE.log
-
-SHORT=at-poly
-SETTINGS=~/settings/$SHORT
-
-ISABELLE_TOOL=$ISABELLE_DEVEL/bin/isabelle
-    
-
-MAIL=$HOME/bin/pmail
-
-TMP=/tmp/isatest-doc.mail.tmp
-while [ -e $TMP ]; do TMP=$TMP.x; done
-
-#
-PRG="$(basename "$0")"
-
-## functions
-
-function usage()
-{
-  echo
-  echo "Usage: $PRG"
-  echo
-  echo "  Run IsaMakefile for every Doc/ subdirectory"
-  echo 
-  exit 1
-}
-
-function fail()
-{
-  echo "$1" >&2
-  exit 2
-}
-
-## 
-
-[ "$#" != "0" ] && usage
-
-if [ -f "$RUNNING/$SHORT.running" -o -e $ERRORLOG ]; then
-  log "Skipped test. Isabelle devel version broken."
-  exit 1
-fi
-cat $SETTINGS >> $ISABELLE_DEVEL/etc/settings
-
-
-echo "Start test at `date`" > $LOG
-echo >> $LOG
-
-cd $DOCDIR || fail "could not cd to $DOCDIR"
-
-# run test
-FAIL="";
-
-cd $DOCDIR
-for DIR in */; do
-  if [ -f "$DIR/IsaMakefile" ]; then
-    echo "Testing [$DIR]" >> $LOG
-    (
-      cd $DIR
-      ulimit -t $MAXTIME 
-      nice $ISABELLE_TOOL make >> $LOG 2>&1
-    ) || FAIL="${FAIL}${DIR} "    
-    echo "Finished [$DIR]" >> $LOG
-    echo >> $LOG
-  fi
-done
-
-ELAPSED=$("$HOME/bin/showtime" "$SECONDS")
-
-echo >> $LOG
-echo "End test on `date`, elapsed time: $ELAPSED" >> $LOG
-
-# send email if there was a problem
-if [ "$FAIL" != "" ]; then
-  echo >> $LOG
-  echo "Failed sessions: ${FAIL}" >> $LOG
-
-  log "doc test FAILED for ${FAIL}, elapsed time $ELAPSED."
-
-  cat > $TMP <<EOF
-Session(s) ${FAIL} in the documentation test failed (log attached).
-Test ended on: $HOSTNAME, `date`.
-
-Have a nice day,
-  isatest
-
-EOF
-
-  for R in $MAILTO; do
-    $MAIL 'doc test failed' "$R" $TMP $LOG
-  done
-
-  rm -f $TMP
-
-  exit 1
-else
-  log "doc test successful, elapsed time $ELAPSED."
-fi
-
diff -r e24bfa4e3b84 -r 88ff12baccba Admin/isatest/isatest-makeall
--- a/Admin/isatest/isatest-makeall	Mon Jul 30 16:03:25 2012 +0200
+++ b/Admin/isatest/isatest-makeall	Mon Jul 30 16:40:21 2012 +0200
@@ -2,7 +2,7 @@
 #
 # Author: Gerwin Klein, TU Muenchen
 #
-# DESCRIPTION: Run isabelle makeall from specified distribution and settings.
+# DESCRIPTION: Run isabelle build from specified distribution and settings.
 
 ## global settings
 . ~/admin/isatest/isatest-settings
@@ -18,14 +18,14 @@
 function usage()
 {
   echo
-  echo "Usage: $PRG [-l logic targets] settings1 [settings2 ...]"
+  echo "Usage: $PRG [-l targets] settings1 [settings2 ...]"
   echo
-  echo "  Runs isabelle makeall for specified settings."
+  echo "  Runs isabelle build for specified settings."
   echo "  Leaves messages in ${ERRORLOG} and ${LOGPREFIX} if it fails."
   echo
   echo "Examples:"
   echo "  $PRG ~/settings/at-poly ~/settings/at-sml"
-  echo "  $PRG -l HOL \"HOL-Library HOL-Bali\" ~/settings/at-poly"
+  echo "  $PRG -l \"HOL-Library HOL-Bali\" ~/settings/at-poly"
   exit 1
 }
 
@@ -46,43 +46,32 @@
 
 [ -d $DISTPREFIX ] || fail "$DISTPREFIX is not a directory."
 
-TARGETS=all
-
-# make file flags and nice setup for different target platforms
-MFLAGS="-k"
+# build args and nice setup for different target platforms
+BUILD_ARGS="-v"
 NICE="nice"
 case $HOSTNAME in
     macbroy2 | macbroy6 | macbroy30)
         NICE=""
         ;;
     lxbroy[234])
-        MFLAGS="-k -j 2"
+        BUILD_ARGS="$BUILD_ARGS -j 2"
         NICE=""
         ;;
 
 esac
 
 ISABELLE_TOOL="$DISTPREFIX/Isabelle/bin/isabelle"
+[ -x $ISABELLE_TOOL ] || fail "Cannot run $ISABELLE_TOOL"
 
-[ -x $ISABELLE_TOOL ] || fail "Cannot run $ISABELLE_TOOL"
+ISABELLE_HOME="$($ISABELLE_TOOL getenv -b ISABELLE_HOME)"
 
 if [ "$1" = "-l" ]; then
   shift
-  [ "$#" -lt "3" ] && usage
-  LOGIC="$1"
-  TARGETS="$2"
-  shift 2
-  ISABELLE_HOME="$($ISABELLE_TOOL getenv -b ISABELLE_HOME)"
-  if [ "$LOGIC" = "." ]; then
-    DIR="."
-    TOOL="$ISABELLE_TOOL makeall $MFLAGS $TARGETS"
-  else
-    DIR="$ISABELLE_HOME/src/$LOGIC"
-    TOOL="$ISABELLE_TOOL make $MFLAGS $TARGETS"
-  fi
+  [ "$#" -lt 2 ] && usage
+  BUILD_ARGS="$BUILD_ARGS $1"
+  shift
 else
-  DIR="."
-  TOOL="$ISABELLE_TOOL makeall $MFLAGS $TARGETS"
+  BUILD_ARGS="$BUILD_ARGS -a"
 fi
 
 IDENT=$(cat "$DISTPREFIX/ISABELLE_IDENT")
@@ -124,7 +113,7 @@
 
     cp $DISTPREFIX/Isabelle/etc/settings.orig $DISTPREFIX/Isabelle/etc/settings
     cat $SETTINGS >> $DISTPREFIX/Isabelle/etc/settings
-    (ulimit -t $MAXTIME; cd $DIR; $NICE $TOOL >> $TESTLOG 2>&1)
+    (ulimit -t $MAXTIME; $NICE "$ISABELLE_TOOL" build $BUILD_ARGS >> $TESTLOG 2>&1)
 
     if [ $? -eq 0 ]
     then
diff -r e24bfa4e3b84 -r 88ff12baccba Admin/isatest/isatest-makedist
--- a/Admin/isatest/isatest-makedist	Mon Jul 30 16:03:25 2012 +0200
+++ b/Admin/isatest/isatest-makedist	Mon Jul 30 16:40:21 2012 +0200
@@ -60,7 +60,7 @@
 
 echo "### building distribution"  >> $DISTLOG 2>&1
 mkdir -p $DISTPREFIX
-$MAKEDIST -j "/home/isabelle/contrib_devel/jedit_build-20120414" >> $DISTLOG 2>&1
+$MAKEDIST -D -j "/home/isabelle/contrib_devel/jedit_build-20120414" >> $DISTLOG 2>&1
 
 if [ $? -ne 0 ]
 then
@@ -105,13 +105,13 @@
 sleep 15
 $SSH lxbroy3 "
   $MAKEALL $HOME/settings/at64-poly;
-  $MAKEALL -l HOL HOL-Library $HOME/settings/at-sml-dev-e"
+  $MAKEALL -l HOL-Library $HOME/settings/at-sml-dev-e"
 sleep 15
 $SSH macbroy23 "$MAKEALL $HOME/settings/at-poly-e"
 sleep 15
 $SSH macbroy2 "
-  $MAKEALL -l . full $HOME/settings/mac-poly64-M4;
-  $MAKEALL -l . full $HOME/settings/mac-poly64-M8;
+  env ISABELLE_BENCHMARK=true $MAKEALL $HOME/settings/mac-poly64-M4;
+  env ISABELLE_BENCHMARK=true $MAKEALL $HOME/settings/mac-poly64-M8;
   $MAKEALL $HOME/settings/mac-poly-M4;
   $MAKEALL $HOME/settings/mac-poly-M8"
 sleep 15