Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
more explicit command-line option for isabelle build;
authorwenzelm
Tue, 14 Jul 2015 19:08:27 +0200
changeset 60724 4fce5d462afc
parent 60723 757cad5a3fe9
child 60725 daf200e2d79a
more explicit command-line option for isabelle build;
Admin/isatest/isatest-makeall file | annotate | diff | comparison | revisions
Admin/isatest/isatest-makedist file | annotate | diff | comparison | revisions
Admin/isatest/settings/at64-poly file | annotate | diff | comparison | revisions 
--- a/Admin/isatest/isatest-makeall	Tue Jul 14 19:01:46 2015 +0200
+++ b/Admin/isatest/isatest-makeall	Tue Jul 14 19:08:27 2015 +0200
@@ -18,7 +18,7 @@
 function usage()
 {
   echo
-  echo "Usage: $PRG [-l targets] settings1 [settings2 ...]"
+  echo "Usage: $PRG [-x SESSION] [-l SESSIONS] settings1 [settings2 ...]"
   echo
   echo "  Runs isabelle build for specified settings."
   echo "  Leaves messages in ${ERRORLOG} and ${LOGPREFIX} if it fails."
@@ -47,6 +47,7 @@
 [ -d $DISTPREFIX ] || fail "$DISTPREFIX is not a directory."
 
 # build args and nice setup for different target platforms
+BUILD_OPTS=""
 BUILD_ARGS="-v"
 NICE="nice"
 case $HOSTNAME in
@@ -65,6 +66,13 @@
 
 ISABELLE_HOME="$($ISABELLE_TOOL getenv -b ISABELLE_HOME)"
 
+if [ "$1" = "-x" ]; then
+  shift
+  [ "$#" -lt 2 ] && usage
+  BUILD_OPTS="$BUILD_OPTS -x $1"
+  shift
+fi
+
 if [ "$1" = "-l" ]; then
   shift
   [ "$#" -lt 2 ] && usage
@@ -122,7 +130,7 @@
 
     cp $DISTPREFIX/Isabelle/etc/settings.orig $DISTPREFIX/Isabelle/etc/settings
     cat $SETTINGS >> $DISTPREFIX/Isabelle/etc/settings
-    (ulimit -t $MAXTIME; $NICE "$ISABELLE_TOOL" build $BUILD_ARGS >> $TESTLOG 2>&1)
+    (ulimit -t $MAXTIME; $NICE "$ISABELLE_TOOL" build $BUILD_OPTS -- $BUILD_ARGS >> $TESTLOG 2>&1)
 
     if [ $? -eq 0 ]
     then
--- a/Admin/isatest/isatest-makedist	Tue Jul 14 19:01:46 2015 +0200
+++ b/Admin/isatest/isatest-makedist	Tue Jul 14 19:08:27 2015 +0200
@@ -100,7 +100,7 @@
 
 ## spawn test runs
 
-$SSH lxbroy10 "$MAKEALL $HOME/settings/at64-poly"
+$SSH lxbroy10 "$MAKEALL -x HOL-Proofs $HOME/settings/at64-poly"
 sleep 15
 $SSH lxbroy4 "
   $MAKEALL -l HOL-Library $HOME/settings/at-poly;
--- a/Admin/isatest/settings/at64-poly	Tue Jul 14 19:01:46 2015 +0200
+++ b/Admin/isatest/settings/at64-poly	Tue Jul 14 19:08:27 2015 +0200
@@ -22,4 +22,4 @@
 ISABELLE_OUTPUT="$ISABELLE_HOME_USER/heaps"
 ISABELLE_BROWSER_INFO="$ISABELLE_HOME_USER/browser_info"
 
-ISABELLE_BUILD_OPTIONS="threads=1 -x HOL-Proofs"
+ISABELLE_BUILD_OPTIONS="threads=1"
isabelle