From: Ferruccio Guidi <ferruccio.guidi@unibo.it>
Date: Fri, 3 Jun 2011 13:40:38 +0000 (+0000)
Subject: Max width overflows, which cause auto to fail, are now logged as errors.
X-Git-Tag: make_still_working~2464
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=1abd18f614b6691547662cc8608f259233b246c7;p=helm.git

Max width overflows, which cause auto to fail, are now logged as errors.
The message "auto gave up" is not very informative by itself!
---

diff --git a/matita/components/ng_tactics/nnAuto.ml b/matita/components/ng_tactics/nnAuto.ml
index 7d57a9785..359b5b076 100644
--- a/matita/components/ng_tactics/nnAuto.ml
+++ b/matita/components/ng_tactics/nnAuto.ml
@@ -1510,10 +1510,12 @@ let rec auto_clusters ?(top=false)
     let classes = HExtlib.clusters (deps status) all_goals in
     List.iter 
 	(fun gl ->
-	   if List.length gl > flags.maxwidth then 
-	     (debug_print ~depth (lazy "FAIL GLOBAL WIDTH"); 
-	      raise (Gaveup IntSet.empty))
-	   else ()) classes;
+	   if List.length gl > flags.maxwidth then begin
+	      debug_print ~depth (lazy "FAIL GLOBAL WIDTH"); 
+	      HLog.error (sprintf "global width (%u) exceeded: %u"
+	         flags.maxwidth (List.length gl));
+	      raise (Gaveup IntSet.empty)
+	   end else ()) classes;
     if List.length classes = 1 then
       let flags = 
         {flags with last = (List.length all_goals = 1)} in 
@@ -1595,9 +1597,12 @@ auto_main flags signature cache depth status: unit =
 	else
         let ng = List.length goals in
         (* moved inside auto_clusters *)
-        if ng > flags.maxwidth then 
-          (print ~depth (lazy "FAIL LOCAL WIDTH"); raise (Gaveup IntSet.empty))
-        else if depth = flags.maxdepth then 
+        if ng > flags.maxwidth then begin 
+          debug_print ~depth (lazy "FAIL LOCAL WIDTH");
+	  HLog.error (sprintf "local width (%u) exceeded: %u"
+	     flags.maxwidth ng);
+	  raise (Gaveup IntSet.empty)
+        end else if depth = flags.maxdepth then
 	  raise (Gaveup IntSet.empty)
         else 
         let status = NTactics.branch_tac ~force:true status in