add option for unify trace (now disabled by default as printing is excessive and rarely used);

--- a/NEWS	Wed Feb 28 15:19:15 2024 +0100
+++ b/NEWS	Wed Feb 28 17:25:54 2024 +0100
@@ -62,6 +62,11 @@
       transp_on_multp
 
 
+*** Pure ***
+
+* Added configuration option for unifier tracing, which is now disabled by default.
+
+
 *** ML ***
 
 * ML antiquotation "try" provides variants of exception handling that

--- a/src/Doc/Isar_Ref/Generic.thy	Wed Feb 28 15:19:15 2024 +0100
+++ b/src/Doc/Isar_Ref/Generic.thy	Wed Feb 28 17:25:54 2024 +0100
@@ -1826,6 +1826,7 @@
 
 text \<open>
   \begin{tabular}{rcll}
+    @{attribute_def unify_trace} & : & \<open>attribute\<close> & default \<open>false\<close> \\
     @{attribute_def unify_trace_simp} & : & \<open>attribute\<close> & default \<open>false\<close> \\
     @{attribute_def unify_trace_types} & : & \<open>attribute\<close> & default \<open>false\<close> \\
     @{attribute_def unify_trace_bound} & : & \<open>attribute\<close> & default \<open>50\<close> \\
@@ -1837,10 +1838,13 @@
   but sometimes needs extra care to identify problems.  These tracing
   options may help.
 
+  \<^descr> @{attribute unify_trace} controls whether unify trace messages will be 
+  printed (controlled via more fine-grained tracing options below).
+
   \<^descr> @{attribute unify_trace_simp} controls tracing of the
   simplification phase of higher-order unification.
 
-  \<^descr> @{attribute unify_trace_types} controls warnings of
+  \<^descr> @{attribute unify_trace_types} controls tracing of potential
   incompleteness, when unification is not considering all possible
   instantiations of schematic type variables.
 

--- a/src/Doc/Logics/document/HOL.tex	Wed Feb 28 15:19:15 2024 +0100
+++ b/src/Doc/Logics/document/HOL.tex	Wed Feb 28 17:25:54 2024 +0100
@@ -176,9 +176,10 @@
   Where function types are involved, Isabelle's unification code does not
   guarantee to find instantiations for type variables automatically.  Be
   prepared to use \ttindex{res_inst_tac} instead of \texttt{resolve_tac},
-  possibly instantiating type variables.  Setting
-  \ttindex{Unify.unify_trace_types} to \texttt{true} causes Isabelle to report
-  omitted search paths during unification.\index{tracing!of unification}
+  possibly instantiating type variables.  Setting \ttindex{Unify.unify_trace}
+  in combination with \ttindex{Unify.unify_trace_types} to \texttt{true} causes
+  Isabelle to report omitted search paths during unification.
+  \index{tracing!of unification}
 \end{warn}
 
 

--- a/src/HOL/Tools/try0.ML	Wed Feb 28 15:19:15 2024 +0100
+++ b/src/HOL/Tools/try0.ML	Wed Feb 28 17:25:54 2024 +0100
@@ -109,12 +109,12 @@
       ctxt
       |> Simplifier_Trace.disable
       |> Context_Position.set_visible false
-      |> Config.put Unify.unify_trace_bound (Config.get ctxt Unify.search_bound)
+      |> Config.put Unify.unify_trace false
       |> Config.put Argo_Tactic.trace "none"
       |> Proof_Context.background_theory (fn thy =>
           thy
           |> Context_Position.set_visible_global false
-          |> Config.put_global Unify.unify_trace_bound (Config.get_global thy Unify.search_bound)));
+          |> Config.put_global Unify.unify_trace false));
 
 fun generic_try0 mode timeout_opt quad st =
   let

--- a/src/Pure/Isar/attrib.ML	Wed Feb 28 15:19:15 2024 +0100
+++ b/src/Pure/Isar/attrib.ML	Wed Feb 28 17:25:54 2024 +0100
@@ -631,6 +631,7 @@
   register_config_bool Thm.show_tags #>
   register_config_bool Pattern.unify_trace_failure #>
   register_config_int Unify.search_bound #>
+  register_config_bool Unify.unify_trace #>
   register_config_int Unify.unify_trace_bound #>
   register_config_bool Unify.unify_trace_simp #>
   register_config_bool Unify.unify_trace_types #>

--- a/src/Pure/unify.ML	Wed Feb 28 15:19:15 2024 +0100
+++ b/src/Pure/unify.ML	Wed Feb 28 17:25:54 2024 +0100
@@ -12,6 +12,7 @@
 signature UNIFY =
 sig
   val search_bound: int Config.T
+  val unify_trace: bool Config.T
   val unify_trace_bound: int Config.T
   val unify_trace_simp: bool Config.T
   val unify_trace_types: bool Config.T
@@ -33,6 +34,8 @@
 
 (* diagnostics *)
 
+val unify_trace = Config.declare_bool ("unify_trace", \<^here>) (K false);
+
 (*tracing starts above this depth, 0 for full*)
 val unify_trace_bound = Config.declare_int ("unify_trace_bound", \<^here>) (K 50);
 
@@ -42,6 +45,11 @@
 (*announce potential incompleteness of type unification*)
 val unify_trace_types = Config.declare_bool ("unify_trace_types", \<^here>) (K false);
 
+fun cond_tracing ctxt msg =
+  if Config.get_generic ctxt unify_trace andalso Context_Position.is_visible_generic ctxt then
+    tracing (msg ())
+  else ();
+
 
 type binderlist = (string * typ) list;
 
@@ -181,13 +189,11 @@
 
 fun test_unify_types context (T, U) env =
   let
-    fun trace () =
-      if Context_Position.is_visible_generic context then
-        let val str_of = Syntax.string_of_typ (Context.proof_of context)
-        in tracing ("Potential loss of completeness: " ^ str_of U ^ " = " ^ str_of T) end
-      else ();
+    fun msg () =
+      let val str_of = Syntax.string_of_typ (Context.proof_of context)
+      in "Potential loss of completeness: " ^ str_of U ^ " = " ^ str_of T end
     val env' = unify_types context (T, U) env;
-  in if is_TVar T orelse is_TVar U then trace () else (); env' end;
+  in if is_TVar T orelse is_TVar U then cond_tracing context msg else (); env' end;
 
 (*Is the term eta-convertible to a single variable with the given rbinder?
   Examples: ?a   ?f(B.0)   ?g(B.1,B.0)
@@ -568,17 +574,18 @@
   In t \<equiv> u print u first because it may be rigid or flexible --
     t is always flexible.*)
 fun print_dpairs context msg (env, dpairs) =
-  if Context_Position.is_visible_generic context then
-    let
-      fun pdp (rbinder, t, u) =
-        let
-          val ctxt = Context.proof_of context;
-          fun termT t =
-            Syntax.pretty_term ctxt (Envir.norm_term env (Logic.rlist_abs (rbinder, t)));
-          val prt = Pretty.blk (0, [termT u, Pretty.str " \<equiv>\<^sup>?", Pretty.brk 1, termT t]);
-        in tracing (Pretty.string_of prt) end;
-    in tracing msg; List.app pdp dpairs end
-  else ();
+  let
+    fun pdp (rbinder, t, u) =
+      let
+        val ctxt = Context.proof_of context;
+        fun termT t =
+          Syntax.pretty_term ctxt (Envir.norm_term env (Logic.rlist_abs (rbinder, t)));
+        val prt = Pretty.blk (0, [termT u, Pretty.str " \<equiv>\<^sup>?", Pretty.brk 1, termT t]);
+      in Pretty.string_of prt end;
+  in
+    cond_tracing context (fn () => msg);
+    List.app (fn dp => cond_tracing context (fn () => pdp dp)) dpairs
+  end;
 
 
 (*Unify the dpairs in the environment.
@@ -602,8 +609,9 @@
             [] => SOME (fold_rev (add_ffpair context) flexflex (env', []), reseq)
           | dp :: frigid' =>
               if tdepth > search_bound then
-                (if Context_Position.is_visible_generic context
-                 then warning "Unification bound exceeded" else (); Seq.pull reseq)
+                (if Context_Position.is_visible_generic context then
+                   warning "Unification bound exceeded -- see unify trace for details"
+                 else (); Seq.pull reseq)
               else
                (if tdepth > unify_trace_bound then
                   print_dpairs context "Enter MATCH" (env',flexrigid@flexflex)
@@ -612,8 +620,8 @@
                     (add_unify (tdepth + 1)) (MATCH context (env',dp, frigid'@flexflex), reseq))))
         end
         handle CANTUNIFY =>
-         (if tdepth > unify_trace_bound andalso Context_Position.is_visible_generic context
-          then tracing "Failure node"
+         (if tdepth > unify_trace_bound
+          then cond_tracing context (fn () => "Failure node")
           else (); Seq.pull reseq));
     val dps = map (fn (t, u) => (binders, t, u)) tus;
   in add_unify 1 ((env, dps), Seq.empty) end;