# HG changeset patch
# User blanchet
# Date 1280424402 -7200
# Node ID d01b8119b2e0eb94fd72ac20a0ba77d055f827a6
# Parent  ff1d4078fe9ab410b5d0c01a73f8612771184767
better error and minimizer output

diff -r ff1d4078fe9a -r d01b8119b2e0 src/HOL/Tools/ATP/atp_systems.ML
--- a/src/HOL/Tools/ATP/atp_systems.ML	Thu Jul 29 19:03:46 2010 +0200
+++ b/src/HOL/Tools/ATP/atp_systems.ML	Thu Jul 29 19:26:42 2010 +0200
@@ -60,7 +60,7 @@
 fun string_for_failure Unprovable = "The ATP problem is unprovable."
   | string_for_failure IncompleteUnprovable =
     "The ATP cannot prove the problem."
-  | string_for_failure CantConnect = "Can't connect to remote ATP."
+  | string_for_failure CantConnect = "Can't connect to remote server."
   | string_for_failure TimedOut = "Timed out."
   | string_for_failure OutOfResources = "The ATP ran out of resources."
   | string_for_failure OldSpass =
@@ -86,7 +86,8 @@
   #> Option.map fst
 
 val known_perl_failures =
-  [(NoPerl, "env: perl"),
+  [(CantConnect, "HTTP error"),
+   (NoPerl, "env: perl"),
    (NoLibwwwPerl, "Can't locate HTTP")]
 
 (* named provers *)
@@ -154,7 +155,7 @@
    arguments = fn complete => fn timeout =>
      ("-Auto -PGiven=0 -PProblem=0 -Splits=0 -FullRed=0 -DocProof \
       \-VarWeight=3 -TimeLimit=" ^
-      string_of_int (to_generous_secs timeout div 2))
+      string_of_int ((to_generous_secs timeout + 1) div 2))
      |> not complete ? prefix "-SOS=1 ",
    proof_delims = [("Here is a proof", "Formulae used in the proof")],
    known_failures =
@@ -230,8 +231,7 @@
    proof_delims = insert (op =) tstp_proof_delims proof_delims,
    known_failures =
      known_failures @ known_perl_failures @
-     [(CantConnect, "HTTP-Error"),
-      (TimedOut, "says Timeout")],
+     [(TimedOut, "says Timeout")],
    max_new_relevant_facts_per_iter = max_new_relevant_facts_per_iter,
    prefers_theory_relevant = prefers_theory_relevant,
    explicit_forall = explicit_forall}
diff -r ff1d4078fe9a -r d01b8119b2e0 src/HOL/Tools/ATP/scripts/remote_atp
--- a/src/HOL/Tools/ATP/scripts/remote_atp	Thu Jul 29 19:03:46 2010 +0200
+++ b/src/HOL/Tools/ATP/scripts/remote_atp	Thu Jul 29 19:26:42 2010 +0200
@@ -98,7 +98,7 @@
 if(!$Response->is_success) {
   my $message = $Response->message;
   $message =~ s/ \(Bad hostname ['"][^'"]*['"]\)//;
-  print $message . "\n";
+  print "HTTP error: " . $message . "\n";
   exit(-1);
 } elsif (exists($Options{'w'})) {
   print $Response->content;
diff -r ff1d4078fe9a -r d01b8119b2e0 src/HOL/Tools/Sledgehammer/sledgehammer_fact_minimizer.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact_minimizer.ML	Thu Jul 29 19:03:46 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact_minimizer.ML	Thu Jul 29 19:26:42 2010 +0200
@@ -115,9 +115,13 @@
          val (min_thms, {proof, internal_thm_names, ...}) =
            sublinear_minimize (test_facts new_timeout)
                (filter_used_facts used_thm_names name_thms_pairs) ([], result)
-         val m = length min_thms
+         val n = length min_thms
          val _ = priority (cat_lines
-           ["Minimized: " ^ string_of_int m ^ " theorem" ^ plural_s m] ^ ".")
+           ["Minimized: " ^ string_of_int n ^ " theorem" ^ plural_s n] ^
+            (case filter (String.isPrefix chained_prefix o fst) min_thms of
+               [] => ""
+             | chained => " (including " ^ Int.toString (length chained) ^
+                          " chained)") ^ ".")
        in
          (SOME min_thms,
           proof_text isar_proof