--- 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
--- 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
--- 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
-
--- 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
--- 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