From 1abd18f614b6691547662cc8608f259233b246c7 Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Fri, 3 Jun 2011 13:40:38 +0000 Subject: [PATCH] Max width overflows, which cause auto to fail, are now logged as errors. The message "auto gave up" is not very informative by itself! --- matita/components/ng_tactics/nnAuto.ml | 19 ++++++++++++------- 1 file changed, 12 insertions(+), 7 deletions(-) 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 -- 2.39.2