1.1 --- a/src/HOL/Tools/ATP/atp_systems.ML	Thu Jul 29 19:03:46 2010 +0200
     1.2 +++ b/src/HOL/Tools/ATP/atp_systems.ML	Thu Jul 29 19:26:42 2010 +0200
     1.3 @@ -60,7 +60,7 @@
     1.4  fun string_for_failure Unprovable = "The ATP problem is unprovable."
     1.5    | string_for_failure IncompleteUnprovable =
     1.6      "The ATP cannot prove the problem."
     1.7 -  | string_for_failure CantConnect = "Can't connect to remote ATP."
     1.8 +  | string_for_failure CantConnect = "Can't connect to remote server."
     1.9    | string_for_failure TimedOut = "Timed out."
    1.10    | string_for_failure OutOfResources = "The ATP ran out of resources."
    1.11    | string_for_failure OldSpass =
    1.12 @@ -86,7 +86,8 @@
    1.13    #> Option.map fst
    1.14  
    1.15  val known_perl_failures =
    1.16 -  [(NoPerl, "env: perl"),
    1.17 +  [(CantConnect, "HTTP error"),
    1.18 +   (NoPerl, "env: perl"),
    1.19     (NoLibwwwPerl, "Can't locate HTTP")]
    1.20  
    1.21  (* named provers *)
    1.22 @@ -154,7 +155,7 @@
    1.23     arguments = fn complete => fn timeout =>
    1.24       ("-Auto -PGiven=0 -PProblem=0 -Splits=0 -FullRed=0 -DocProof \
    1.25        \-VarWeight=3 -TimeLimit=" ^
    1.26 -      string_of_int (to_generous_secs timeout div 2))
    1.27 +      string_of_int ((to_generous_secs timeout + 1) div 2))
    1.28       |> not complete ? prefix "-SOS=1 ",
    1.29     proof_delims = [("Here is a proof", "Formulae used in the proof")],
    1.30     known_failures =
    1.31 @@ -230,8 +231,7 @@
    1.32     proof_delims = insert (op =) tstp_proof_delims proof_delims,
    1.33     known_failures =
    1.34       known_failures @ known_perl_failures @
    1.35 -     [(CantConnect, "HTTP-Error"),
    1.36 -      (TimedOut, "says Timeout")],
    1.37 +     [(TimedOut, "says Timeout")],
    1.38     max_new_relevant_facts_per_iter = max_new_relevant_facts_per_iter,
    1.39     prefers_theory_relevant = prefers_theory_relevant,
    1.40     explicit_forall = explicit_forall}

     2.1 --- a/src/HOL/Tools/ATP/scripts/remote_atp	Thu Jul 29 19:03:46 2010 +0200
     2.2 +++ b/src/HOL/Tools/ATP/scripts/remote_atp	Thu Jul 29 19:26:42 2010 +0200
     2.3 @@ -98,7 +98,7 @@
     2.4  if(!$Response->is_success) {
     2.5    my $message = $Response->message;
     2.6    $message =~ s/ \(Bad hostname ['"][^'"]*['"]\)//;
     2.7 -  print $message . "\n";
     2.8 +  print "HTTP error: " . $message . "\n";
     2.9    exit(-1);
    2.10  } elsif (exists($Options{'w'})) {
    2.11    print $Response->content;

     3.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact_minimizer.ML	Thu Jul 29 19:03:46 2010 +0200
     3.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact_minimizer.ML	Thu Jul 29 19:26:42 2010 +0200
     3.3 @@ -115,9 +115,13 @@
     3.4           val (min_thms, {proof, internal_thm_names, ...}) =
     3.5             sublinear_minimize (test_facts new_timeout)
     3.6                 (filter_used_facts used_thm_names name_thms_pairs) ([], result)
     3.7 -         val m = length min_thms
     3.8 +         val n = length min_thms
     3.9           val _ = priority (cat_lines
    3.10 -           ["Minimized: " ^ string_of_int m ^ " theorem" ^ plural_s m] ^ ".")
    3.11 +           ["Minimized: " ^ string_of_int n ^ " theorem" ^ plural_s n] ^
    3.12 +            (case filter (String.isPrefix chained_prefix o fst) min_thms of
    3.13 +               [] => ""
    3.14 +             | chained => " (including " ^ Int.toString (length chained) ^
    3.15 +                          " chained)") ^ ".")
    3.16         in
    3.17           (SOME min_thms,
    3.18            proof_text isar_proof