merged
authorwenzelm
Tue Jul 14 19:08:40 2015 +0200 (2015-07-14)
changeset 60725daf200e2d79a
parent 60721 c1b7793c23a3
parent 60724 4fce5d462afc
child 60726 6d500a224cbe
merged
     1.1 --- a/Admin/isatest/isatest-makeall	Tue Jul 14 13:48:03 2015 +0200
     1.2 +++ b/Admin/isatest/isatest-makeall	Tue Jul 14 19:08:40 2015 +0200
     1.3 @@ -18,7 +18,7 @@
     1.4  function usage()
     1.5  {
     1.6    echo
     1.7 -  echo "Usage: $PRG [-l targets] settings1 [settings2 ...]"
     1.8 +  echo "Usage: $PRG [-x SESSION] [-l SESSIONS] settings1 [settings2 ...]"
     1.9    echo
    1.10    echo "  Runs isabelle build for specified settings."
    1.11    echo "  Leaves messages in ${ERRORLOG} and ${LOGPREFIX} if it fails."
    1.12 @@ -47,6 +47,7 @@
    1.13  [ -d $DISTPREFIX ] || fail "$DISTPREFIX is not a directory."
    1.14  
    1.15  # build args and nice setup for different target platforms
    1.16 +BUILD_OPTS=""
    1.17  BUILD_ARGS="-v"
    1.18  NICE="nice"
    1.19  case $HOSTNAME in
    1.20 @@ -65,6 +66,13 @@
    1.21  
    1.22  ISABELLE_HOME="$($ISABELLE_TOOL getenv -b ISABELLE_HOME)"
    1.23  
    1.24 +if [ "$1" = "-x" ]; then
    1.25 +  shift
    1.26 +  [ "$#" -lt 2 ] && usage
    1.27 +  BUILD_OPTS="$BUILD_OPTS -x $1"
    1.28 +  shift
    1.29 +fi
    1.30 +
    1.31  if [ "$1" = "-l" ]; then
    1.32    shift
    1.33    [ "$#" -lt 2 ] && usage
    1.34 @@ -122,7 +130,7 @@
    1.35  
    1.36      cp $DISTPREFIX/Isabelle/etc/settings.orig $DISTPREFIX/Isabelle/etc/settings
    1.37      cat $SETTINGS >> $DISTPREFIX/Isabelle/etc/settings
    1.38 -    (ulimit -t $MAXTIME; $NICE "$ISABELLE_TOOL" build $BUILD_ARGS >> $TESTLOG 2>&1)
    1.39 +    (ulimit -t $MAXTIME; $NICE "$ISABELLE_TOOL" build $BUILD_OPTS -- $BUILD_ARGS >> $TESTLOG 2>&1)
    1.40  
    1.41      if [ $? -eq 0 ]
    1.42      then
     2.1 --- a/Admin/isatest/isatest-makedist	Tue Jul 14 13:48:03 2015 +0200
     2.2 +++ b/Admin/isatest/isatest-makedist	Tue Jul 14 19:08:40 2015 +0200
     2.3 @@ -100,7 +100,7 @@
     2.4  
     2.5  ## spawn test runs
     2.6  
     2.7 -$SSH lxbroy10 "$MAKEALL $HOME/settings/at64-poly"
     2.8 +$SSH lxbroy10 "$MAKEALL -x HOL-Proofs $HOME/settings/at64-poly"
     2.9  sleep 15
    2.10  $SSH lxbroy4 "
    2.11    $MAKEALL -l HOL-Library $HOME/settings/at-poly;
     3.1 --- a/Admin/isatest/settings/at64-poly	Tue Jul 14 13:48:03 2015 +0200
     3.2 +++ b/Admin/isatest/settings/at64-poly	Tue Jul 14 19:08:40 2015 +0200
     3.3 @@ -22,4 +22,4 @@
     3.4  ISABELLE_OUTPUT="$ISABELLE_HOME_USER/heaps"
     3.5  ISABELLE_BROWSER_INFO="$ISABELLE_HOME_USER/browser_info"
     3.6  
     3.7 -ISABELLE_BUILD_OPTIONS="threads=1 -x HOL-Proofs"
     3.8 +ISABELLE_BUILD_OPTIONS="threads=1"
     4.1 --- a/src/Pure/Isar/proof.ML	Tue Jul 14 13:48:03 2015 +0200
     4.2 +++ b/src/Pure/Isar/proof.ML	Tue Jul 14 19:08:40 2015 +0200
     4.3 @@ -498,7 +498,7 @@
     4.4      fun err_lost () = error ("Lost goal structure:\n" ^ Display.string_of_thm ctxt goal);
     4.5  
     4.6      val th =
     4.7 -      (Goal.conclude (if length (flat propss) > 1 then Thm.norm_proof goal else goal)
     4.8 +      (Goal.conclude (if length (flat propss) > 1 then Thm.close_derivation goal else goal)
     4.9          handle THM _ => err_lost ())
    4.10        |> Drule.flexflex_unique (SOME ctxt)
    4.11        |> Thm.check_shyps (Variable.sorts_of ctxt)
     5.1 --- a/src/Pure/goal.ML	Tue Jul 14 13:48:03 2015 +0200
     5.2 +++ b/src/Pure/goal.ML	Tue Jul 14 19:08:40 2015 +0200
     5.3 @@ -230,7 +230,9 @@
     5.4              result)
     5.5            (Thm.term_of stmt);
     5.6    in
     5.7 -    Conjunction.elim_balanced (length props) res
     5.8 +    res
     5.9 +    |> length props > 1 ? Thm.close_derivation
    5.10 +    |> Conjunction.elim_balanced (length props)
    5.11      |> map (Assumption.export false ctxt' ctxt)
    5.12      |> Variable.export ctxt' ctxt
    5.13      |> map Drule.zero_var_indexes