Commit 893e7668 authored by makarius's avatar makarius
Browse files

replaced ISATOOL by ISABELLE_TOOL;

parent f49165f30a84
#!/usr/bin/env bash
#
# $Id: publish,v 1.10 2008-09-22 09:36:32 lsf37 Exp $
# $Id: publish,v 1.11 2008-10-04 14:29:42 makarius Exp $
# Author: Gerwin Klein, NICTA
#
# publishes archive entry + main web pages on SF
......@@ -58,9 +58,9 @@ function fail()
function check_isatool()
{
[ -x $ISATOOL ] || fail "No isatool found at [$ISATOOL]."
ML_IDENTIFIER=`$ISATOOL getenv -b ML_IDENTIFIER` || fail "could not identify ML system"
ISABELLE_HOME=`$ISATOOL getenv -b ISABELLE_HOME` || fail "could not find Isabelle home"
[ -x $ISABELLE_TOOL ] || fail "No isatool found at [$ISABELLE_TOOL]."
ML_IDENTIFIER=`$ISABELLE_TOOL getenv -b ML_IDENTIFIER` || fail "could not identify ML system"
ISABELLE_HOME=`$ISABELLE_TOOL getenv -b ISABELLE_HOME` || fail "could not find Isabelle home"
export ISABELLE_IMAGE_PATH="$ISABELLE_HOME/heaps/$ML_IDENTIFIER/"
}
......@@ -68,7 +68,7 @@ function check_isatool()
[ "$#" -lt "2" -o "$1" = "-?" ] && usage
ISATOOL=isatool
ISABELLE_TOOL=isatool
INTERACTIVE="yes"
while getopts "t:rf" OPT
......@@ -82,7 +82,7 @@ do
INTERACTIVE="no"
;;
t)
ISATOOL="$OPTARG"
ISABELLE_TOOL="$OPTARG"
check_isatool
;;
esac
......@@ -94,7 +94,7 @@ TAG="$1"
shift
if [ "$USE_RELEASE" == "1" ]; then
ISATOOL="$ISABELLE_RELEASES/$TAG/bin/isatool"
ISABELLE_TOOL="$ISABELLE_RELEASES/$TAG/bin/isatool"
check_isatool
fi
......@@ -132,7 +132,7 @@ if [ "$1" != "-" ]; then
if [ -d $DIR -a "$DIR" != "CVS" ]; then
echo "Generating HTML for [$DIR]"
cd $DIR
$ISATOOL make clean all || fail "isatool make all failed on [$DIR]"
$ISABELLE_TOOL make clean all || fail "isatool make all failed on [$DIR]"
cd ..
echo "Tarring [$DIR]"
$TAR -cf $EXPORT_PRE-$DIR-$DATE.tar $DIR
......
#!/usr/bin/env bash
#
# $Id: regression,v 1.29 2008-06-12 06:57:14 lsf37 Exp $
# $Id: regression,v 1.30 2008-10-04 14:29:42 makarius Exp $
# Author: Gerwin Klein, NICTA
#
# Automated regression test to be run from cron.
......@@ -64,7 +64,7 @@ if [ "$1" == "-" ]; then
TAG="-A"
AFP_VER="development"
WORKING_COPY=$WORKING_COPY/devel
ISATOOL=$ISABELLE_DEVEL/bin/isatool
ISABELLE_TOOL=$ISABELLE_DEVEL/bin/isatool
ERRORDIR=$HOME/var
RUNNING=$HOME/var/running
......@@ -73,21 +73,21 @@ if [ "$1" == "-" ]; then
exit 1
fi
cat $SETTINGS >> $ISABELLE_DEVEL/etc/settings
ML_IDENTIFIER=`$ISATOOL getenv -b ML_IDENTIFIER` || fail "could not identify ML system"
ML_IDENTIFIER=`$ISABELLE_TOOL getenv -b ML_IDENTIFIER` || fail "could not identify ML system"
export ISABELLE_IMAGE_PATH="$HOME/isabelle-$SHORT/heaps/$ML_IDENTIFIER/"
LOG=$LOG-devel-$DATE.log
SNAPSHOT=1;
REPORT=$REPORT-devel
BROWSER_INFO=`$ISATOOL getenv -b ISABELLE_BROWSER_INFO` || fail "could not find browser info"
BROWSER_INFO=`$ISABELLE_TOOL getenv -b ISABELLE_BROWSER_INFO` || fail "could not find browser info"
[ -e "$BROWSER_INFO" ] && rm -rf $BROWSER_INFO
else
TAG="-r $1"
AFP_VER="release ($1)"
WORKING_COPY=$WORKING_COPY/release
ISATOOL=$ISABELLE_RELEASES/$1/bin/isatool
ML_IDENTIFIER=`$ISATOOL getenv -b ML_IDENTIFIER` || fail "could not identify ML system"
ISABELLE_TOOL=$ISABELLE_RELEASES/$1/bin/isatool
ML_IDENTIFIER=`$ISABELLE_TOOL getenv -b ML_IDENTIFIER` || fail "could not identify ML system"
export ISABELLE_IMAGE_PATH="$ISABELLE_RELEASES/$1/heaps/$ML_IDENTIFIER/"
LOG=$LOG-$1-$DATE.log
REPORT=$REPORT-$1
......@@ -108,7 +108,7 @@ echo "end cvs update" >> $LOG
echo >> $LOG
# run test
nice $WORKING_COPY/admin/testall $FRQ -t $ISATOOL -c >> $LOG 2>&1
nice $WORKING_COPY/admin/testall $FRQ -t $ISABELLE_TOOL -c >> $LOG 2>&1
FAILURE=$?
ELAPSED=$("$HOME/bin/showtime" "$SECONDS")
......
#!/usr/bin/env bash
#
# $Id: testall,v 1.7 2006-06-20 22:22:30 lsf37 Exp $
# $Id: testall,v 1.8 2008-10-04 14:29:42 makarius Exp $
# Author: Gerwin Klein, NICTA
#
# Tests all entries in Archive of Formal Proofs
......@@ -46,9 +46,9 @@ function fail()
function check_isatool()
{
[ -x $ISATOOL ] || fail "No isatool found at [$ISATOOL]."
ML_IDENTIFIER=`$ISATOOL getenv -b ML_IDENTIFIER` || fail "could not identify ML system"
ISABELLE_HOME=`$ISATOOL getenv -b ISABELLE_HOME` || fail "could not find Isabelle home"
[ -x $ISABELLE_TOOL ] || fail "No isatool found at [$ISABELLE_TOOL]."
ML_IDENTIFIER=`$ISABELLE_TOOL getenv -b ML_IDENTIFIER` || fail "could not identify ML system"
ISABELLE_HOME=`$ISABELLE_TOOL getenv -b ISABELLE_HOME` || fail "could not find Isabelle home"
[ -n "$ISABELLE_IMAGE_PATH" ] || export ISABELLE_IMAGE_PATH="$ISABELLE_HOME/heaps/$ML_IDENTIFIER/"
}
......@@ -59,7 +59,7 @@ THYS="$(dirname "$0")/../thys"
[ "$1" = "-?" ] && usage
ISATOOL=isatool
ISABELLE_TOOL=isatool
FRQONLY="no"
while getopts "t:cfr:d:" OPT
......@@ -67,7 +67,7 @@ do
case "$OPT" in
r)
[ "$ISABELLE_RELEASES" == "" ] && fail "ISABELLE_RELEASES not set"
ISATOOL="$ISABELLE_RELEASES/$OPTARG/bin/isatool"
ISABELLE_TOOL="$ISABELLE_RELEASES/$OPTARG/bin/isatool"
check_isatool
;;
c)
......@@ -77,7 +77,7 @@ do
THYS="$OPTARG"
;;
t)
ISATOOL="$OPTARG"
ISABELLE_TOOL="$OPTARG"
check_isatool
;;
f)
......@@ -101,7 +101,7 @@ for DIR in $DIRS; do
cd $DIR
if [ "$FRQONLY" == "no" ] || (unset FREQUENT; . ./config; [ "$FREQUENT" == "yes" ]); then
echo "Testing [$DIR]"
$ISATOOL make $CLEAN all $@ || FAIL="${FAIL}${DIR} "
$ISABELLE_TOOL make $CLEAN all $@ || FAIL="${FAIL}${DIR} "
echo "Finished [$DIR]"
fi
cd ..
......
......@@ -27,7 +27,7 @@ IMAGE=$(ISABELLE_IMAGE_PATH)$(BASE-IMAGE)
endif
USEDIR = $(ISATOOL) usedir -v true -i true -V outline=/proof,/ML -d pdf -P "http://isabelle.in.tum.de/library/" # -D generated
USEDIR = $(ISABELLE_TOOL) usedir -v true -i true -V outline=/proof,/ML -d pdf -P "http://isabelle.in.tum.de/library/" # -D generated
# time limit (in sec)
MAXTIME = 3600
......
......@@ -27,7 +27,7 @@ IMAGE=$(ISABELLE_IMAGE_PATH)$(BASE-IMAGE)
endif
USEDIR = $(ISATOOL) usedir -v true -i true -V outline=/proof,/ML -d pdf -P "http://isabelle.in.tum.de/library/" # -D generated
USEDIR = $(ISABELLE_TOOL) usedir -v true -i true -V outline=/proof,/ML -d pdf -P "http://isabelle.in.tum.de/library/" # -D generated
# time limit (in sec)
MAXTIME = 3600
......
......@@ -26,7 +26,7 @@ IMAGE=$(ISABELLE_IMAGE_PATH)$(BASE-IMAGE)
endif
USEDIR = $(ISATOOL) usedir -v true -i true -V outline=/proof,/ML -d pdf -P "http://isabelle.in.tum.de/library/"
USEDIR = $(ISABELLE_TOOL) usedir -v true -i true -V outline=/proof,/ML -d pdf -P "http://isabelle.in.tum.de/library/"
# time limit (in sec)
MAXTIME = 600
......
......@@ -23,7 +23,7 @@ LOG = $(OUT)/log
IMAGE=$(OUT)/$(BASE-IMAGE)
USEDIR = $(ISATOOL) usedir -v true -g true -i true -V outline=/proof,/ML -d pdf # -D generated
USEDIR = $(ISABELLE_TOOL) usedir -v true -g true -i true -V outline=/proof,/ML -d pdf # -D generated
# time limit (in sec)
MAXTIME = 3600
......@@ -34,7 +34,7 @@ MAXTIME = 3600
$(SESSION-NAME): Simpl $(LOG)/$(BASE-IMAGE)-$(SESSION-NAME).gz
Simpl:
cd ../Simpl; $(ISATOOL) make Simpl
cd ../Simpl; $(ISABELLE_TOOL) make Simpl
$(LOG)/$(BASE-IMAGE)-$(SESSION-NAME).gz: $(IMAGE) ROOT.ML *.thy document/*.tex document/*.bib
cd ..; ulimit -t $(MAXTIME); $(USEDIR) $(IMAGE) $(SESSION-NAME)
......
......@@ -27,7 +27,7 @@ IMAGE=$(ISABELLE_IMAGE_PATH)$(BASE-IMAGE)
endif
USEDIR = $(ISATOOL) usedir -v true -i true -V outline=/proof,/ML -d pdf -P "http://isabelle.in.tum.de/library/" # -D generated
USEDIR = $(ISABELLE_TOOL) usedir -v true -i true -V outline=/proof,/ML -d pdf -P "http://isabelle.in.tum.de/library/" # -D generated
# time limit (in sec)
MAXTIME = 3600
......
......@@ -27,7 +27,7 @@ IMAGE=$(ISABELLE_IMAGE_PATH)$(BASE-IMAGE)
endif
USEDIR = $(ISATOOL) usedir -v true -i true -V outline=/proof,/ML -d pdf -P "http://isabelle.in.tum.de/library/" # -D generated
USEDIR = $(ISABELLE_TOOL) usedir -v true -i true -V outline=/proof,/ML -d pdf -P "http://isabelle.in.tum.de/library/" # -D generated
# time limit (in sec)
MAXTIME = 3600
......
......@@ -27,7 +27,7 @@ IMAGE=$(ISABELLE_IMAGE_PATH)$(BASE-IMAGE)
endif
USEDIR = $(ISATOOL) usedir -v true -i true -V outline=/proof,/ML -d pdf -P "http://isabelle.in.tum.de/library/" # -D generated
USEDIR = $(ISABELLE_TOOL) usedir -v true -i true -V outline=/proof,/ML -d pdf -P "http://isabelle.in.tum.de/library/" # -D generated
# time limit (in sec)
MAXTIME = 3600
......
......@@ -31,7 +31,7 @@ IMAGE=$(ISABELLE_IMAGE_PATH)$(BASE-IMAGE)
endif
USEDIR = $(ISATOOL) usedir -v true -i true -V outline=/proof,/ML -d pdf -P "http://isabelle.in.tum.de/library/" # -D generated
USEDIR = $(ISABELLE_TOOL) usedir -v true -i true -V outline=/proof,/ML -d pdf -P "http://isabelle.in.tum.de/library/" # -D generated
# time limit (in sec)
MAXTIME = 3600
......
......@@ -27,7 +27,7 @@ IMAGE=$(ISABELLE_IMAGE_PATH)$(BASE-IMAGE)
endif
USEDIR = $(ISATOOL) usedir -v true -i true -V outline=/proof,/ML -d pdf -P "http://isabelle.in.tum.de/library/" # -D generated
USEDIR = $(ISABELLE_TOOL) usedir -v true -i true -V outline=/proof,/ML -d pdf -P "http://isabelle.in.tum.de/library/" # -D generated
# time limit (in sec)
MAXTIME = 3600
......
......@@ -27,7 +27,7 @@ IMAGE=$(ISABELLE_IMAGE_PATH)$(BASE-IMAGE)
endif
USEDIR = $(ISATOOL) usedir -v true -i true -V outline=/proof,/ML -d pdf -P "http://isabelle.in.tum.de/library/" # -D generated
USEDIR = $(ISABELLE_TOOL) usedir -v true -i true -V outline=/proof,/ML -d pdf -P "http://isabelle.in.tum.de/library/" # -D generated
# time limit (in sec)
MAXTIME = 3600
......
......@@ -24,7 +24,7 @@ else
IMAGE=$(ISABELLE_IMAGE_PATH)$(BASE-IMAGE)
endif
USEDIR = $(ISATOOL) usedir -b -v true -i true -V outline=/proof,/ML -d pdf -P "http://isabelle.in.tum.de/library/" # -D generated
USEDIR = $(ISABELLE_TOOL) usedir -b -v true -i true -V outline=/proof,/ML -d pdf -P "http://isabelle.in.tum.de/library/" # -D generated
# time limit (in sec)
MAXTIME = 2000
......
......@@ -27,7 +27,7 @@ IMAGE=$(ISABELLE_IMAGE_PATH)$(BASE-IMAGE)
endif
USEDIR = $(ISATOOL) usedir -v true -i true -V outline=/proof,/ML -d pdf -P "http://isabelle.in.tum.de/library/" # -D generated
USEDIR = $(ISABELLE_TOOL) usedir -v true -i true -V outline=/proof,/ML -d pdf -P "http://isabelle.in.tum.de/library/" # -D generated
# time limit (in sec)
MAXTIME = 3600
......
......@@ -27,7 +27,7 @@ IMAGE=$(ISABELLE_IMAGE_PATH)$(BASE-IMAGE)
endif
USEDIR = $(ISATOOL) usedir -v true -i true -V outline=/proof,/ML -d pdf -P "http://isabelle.in.tum.de/library/" # -D generated
USEDIR = $(ISABELLE_TOOL) usedir -v true -i true -V outline=/proof,/ML -d pdf -P "http://isabelle.in.tum.de/library/" # -D generated
# time limit (in sec)
MAXTIME = 3600
......
......@@ -27,7 +27,7 @@ IMAGE=$(ISABELLE_IMAGE_PATH)$(BASE-IMAGE)
endif
USEDIR = $(ISATOOL) usedir -v true -i true -V outline=/proof,/ML -d pdf -P "http://isabelle.in.tum.de/library/" # -D generated
USEDIR = $(ISABELLE_TOOL) usedir -v true -i true -V outline=/proof,/ML -d pdf -P "http://isabelle.in.tum.de/library/" # -D generated
# time limit (in sec)
MAXTIME = 3600
......
......@@ -27,7 +27,7 @@ IMAGE=$(ISABELLE_IMAGE_PATH)$(BASE-IMAGE)
endif
USEDIR = $(ISATOOL) usedir -v true -i true -V outline=/proof,/ML -d pdf -P "http://isabelle.in.tum.de/library/" # -D generated
USEDIR = $(ISABELLE_TOOL) usedir -v true -i true -V outline=/proof,/ML -d pdf -P "http://isabelle.in.tum.de/library/" # -D generated
# time limit (in sec)
MAXTIME = 3600
......
......@@ -27,7 +27,7 @@ IMAGE=$(ISABELLE_IMAGE_PATH)$(BASE-IMAGE)
endif
USEDIR = $(ISATOOL) usedir -v true -i true -V outline=/proof,/ML -d pdf -P "http://isabelle.in.tum.de/library/" # -D generated
USEDIR = $(ISABELLE_TOOL) usedir -v true -i true -V outline=/proof,/ML -d pdf -P "http://isabelle.in.tum.de/library/" # -D generated
# time limit (in sec)
MAXTIME = 3600
......
......@@ -27,7 +27,7 @@ IMAGE=$(ISABELLE_IMAGE_PATH)$(BASE-IMAGE)
endif
USEDIR = $(ISATOOL) usedir -v true -i true -V outline=/proof,/ML -d pdf -P "http://isabelle.in.tum.de/library/" # -D generated
USEDIR = $(ISABELLE_TOOL) usedir -v true -i true -V outline=/proof,/ML -d pdf -P "http://isabelle.in.tum.de/library/" # -D generated
# time limit (in sec)
MAXTIME = 3600
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment