# HG changeset patch # User wenzelm # Date 1436893720 -7200 # Node ID daf200e2d79ab2b30aed43b4668429b38a0fc55d # Parent c1b7793c23a31410736eae9d6ccfb7e8659ed7d0# Parent 4fce5d462afc432f00128f01bf378e06de026330 merged diff -r c1b7793c23a3 -r daf200e2d79a Admin/isatest/isatest-makeall --- a/Admin/isatest/isatest-makeall Tue Jul 14 13:48:03 2015 +0200 +++ b/Admin/isatest/isatest-makeall Tue Jul 14 19:08:40 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 diff -r c1b7793c23a3 -r daf200e2d79a Admin/isatest/isatest-makedist --- a/Admin/isatest/isatest-makedist Tue Jul 14 13:48:03 2015 +0200 +++ b/Admin/isatest/isatest-makedist Tue Jul 14 19:08:40 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; diff -r c1b7793c23a3 -r daf200e2d79a Admin/isatest/settings/at64-poly --- a/Admin/isatest/settings/at64-poly Tue Jul 14 13:48:03 2015 +0200 +++ b/Admin/isatest/settings/at64-poly Tue Jul 14 19:08:40 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" diff -r c1b7793c23a3 -r daf200e2d79a src/Pure/Isar/proof.ML --- a/src/Pure/Isar/proof.ML Tue Jul 14 13:48:03 2015 +0200 +++ b/src/Pure/Isar/proof.ML Tue Jul 14 19:08:40 2015 +0200 @@ -498,7 +498,7 @@ fun err_lost () = error ("Lost goal structure:\n" ^ Display.string_of_thm ctxt goal); val th = - (Goal.conclude (if length (flat propss) > 1 then Thm.norm_proof goal else goal) + (Goal.conclude (if length (flat propss) > 1 then Thm.close_derivation goal else goal) handle THM _ => err_lost ()) |> Drule.flexflex_unique (SOME ctxt) |> Thm.check_shyps (Variable.sorts_of ctxt) diff -r c1b7793c23a3 -r daf200e2d79a src/Pure/goal.ML --- a/src/Pure/goal.ML Tue Jul 14 13:48:03 2015 +0200 +++ b/src/Pure/goal.ML Tue Jul 14 19:08:40 2015 +0200 @@ -230,7 +230,9 @@ result) (Thm.term_of stmt); in - Conjunction.elim_balanced (length props) res + res + |> length props > 1 ? Thm.close_derivation + |> Conjunction.elim_balanced (length props) |> map (Assumption.export false ctxt' ctxt) |> Variable.export ctxt' ctxt |> map Drule.zero_var_indexes