Merge PR #9142: Disable Ltac backtraces

Ack-by: Zimmi48
Reviewed-by: jfehrle
Ack-by: ppedrot

12 files changed, 51 insertions, 21 deletions

diff --git a/CHANGES.md b/CHANGES.md
index 08519eb1fb..d0774276ad 100644
--- a/CHANGES.md
+++ b/CHANGES.md
@@ -95,6 +95,8 @@ Tactics
   by posing the specifying equation for `Z.div` and `Z.modulo` before
   replacing them with atoms.
 
+- Ltac backtraces can be turned on using the "Ltac Backtrace" option.
+
 Vernacular commands
 
 - `Combined Scheme` can now work when inductive schemes are generated in sort
diff --git a/doc/sphinx/proof-engine/ltac.rst b/doc/sphinx/proof-engine/ltac.rst
index 4f486a777d..c134563efe 100644
--- a/doc/sphinx/proof-engine/ltac.rst
+++ b/doc/sphinx/proof-engine/ltac.rst
@@ -1162,6 +1162,15 @@ Printing |Ltac| tactics
 Debugging |Ltac| tactics
 ------------------------
 
+Backtraces
+~~~~~~~~~~
+
+.. flag:: Ltac Backtrace
+
+   Setting this flag displays a backtrace on Ltac failures that can be useful
+   to find out what went wrong. It is disabled by default for performance
+   reasons.
+
 Info trace
 ~~~~~~~~~~
 
diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml
index 62906303a4..30f716d764 100644
--- a/plugins/ltac/tacinterp.ml
+++ b/plugins/ltac/tacinterp.ml
@@ -117,9 +117,14 @@ let combine_appl appl1 appl2 =
 let of_tacvalue v = in_gen (topwit wit_tacvalue) v
 let to_tacvalue v = out_gen (topwit wit_tacvalue) v
 
+let log_trace = ref false
+
+let is_traced () =
+  !log_trace || !Flags.profile_ltac
+
 (** More naming applications *)
 let name_vfun appl vle =
-  if has_type vle (topwit wit_tacvalue) then
+  if is_traced () && has_type vle (topwit wit_tacvalue) then
     match to_tacvalue vle with
     | VFun (appl0,trace,lfun,vars,t) -> of_tacvalue (VFun (combine_appl appl0 appl,trace,lfun,vars,t))
     | _ -> vle
@@ -137,9 +142,11 @@ type interp_sign = Geninterp.interp_sign = {
   lfun : value Id.Map.t;
   extra : TacStore.t }
 
-let extract_trace ist = match TacStore.get ist.extra f_trace with
-| None -> []
-| Some l -> l
+let extract_trace ist =
+  if is_traced () then match TacStore.get ist.extra f_trace with
+  | None -> []
+  | Some l -> l
+  else []
 
 let print_top_val env v = Pptactic.pr_value Pptactic.ltop v
 
@@ -161,8 +168,11 @@ let catch_error call_trace f x =
     let e = CErrors.push e in
     catching_error call_trace iraise e
 
+let wrap_error tac k =
+  if is_traced () then Proofview.tclORELSE tac k else tac
+
 let catch_error_tac call_trace tac =
-  Proofview.tclORELSE
+  wrap_error
     tac
     (catching_error call_trace (fun (e, info) -> Proofview.tclZERO ~info e))
 
@@ -203,9 +213,11 @@ let constr_of_id env id =
 (** Generic arguments : table of interpretation functions *)
 
 (* Some of the code further down depends on the fact that push_trace does not modify sigma (the evar map) *)
-let push_trace call ist = match TacStore.get ist.extra f_trace with
-| None -> Proofview.tclUNIT [call]
-| Some trace -> Proofview.tclUNIT (call :: trace)
+let push_trace call ist =
+  if is_traced () then match TacStore.get ist.extra f_trace with
+  | None -> Proofview.tclUNIT [call]
+  | Some trace -> Proofview.tclUNIT (call :: trace)
+  else Proofview.tclUNIT []
 
 let propagate_trace ist loc id v =
   if has_type v (topwit wit_tacvalue) then
@@ -1263,7 +1275,7 @@ and interp_app loc ist fv largs : Val.t Ftactic.t =
         let fold accu (id, v) = Id.Map.add id v accu in
 	let newlfun = List.fold_left fold olfun extfun in
       if List.is_empty lvar then
-        begin Proofview.tclORELSE
+        begin wrap_error
             begin
               let ist = {
                 lfun = newlfun;
@@ -1423,7 +1435,7 @@ and interp_match_successes lz ist s =
 (* Interprets the Match expressions *)
 and interp_match ist lz constr lmr =
   let (>>=) = Ftactic.bind in
-  begin Proofview.tclORELSE
+  begin wrap_error
     (interp_ltac_constr ist constr)
     begin function
       | (e, info) ->
@@ -1509,7 +1521,7 @@ and interp_genarg_var_list ist x =
 (* Interprets tactic expressions : returns a "constr" *)
 and interp_ltac_constr ist e : EConstr.t Ftactic.t =
   let (>>=) = Ftactic.bind in
-  begin Proofview.tclORELSE
+  begin wrap_error
       (val_interp ist e)
       begin function (err, info) -> match err with
         | Not_found ->
@@ -2076,4 +2088,13 @@ let () =
       optread  = (fun () -> get_debug () != Tactic_debug.DebugOff);
       optwrite = vernac_debug }
 
+let () =
+  let open Goptions in
+  declare_bool_option
+    { optdepr  = false;
+      optname  = "Ltac Backtrace";
+      optkey   = ["Ltac"; "Backtrace"];
+      optread  = (fun () -> !log_trace);
+      optwrite = (fun b -> log_trace := b) }
+
 let () = Hook.set Vernacentries.interp_redexp_hook interp_redexp
diff --git a/test-suite/output/Errors.v b/test-suite/output/Errors.v
index edc35f17b4..b52537dec0 100644
--- a/test-suite/output/Errors.v
+++ b/test-suite/output/Errors.v
@@ -1,6 +1,8 @@
 (* coq-prog-args: ("-top" "Errors") *)
 (* Test error messages *)
 
+Set Ltac Backtrace.
+
 (* Test non-regression of bug fixed in r13486 (bad printer for module names) *)
 
 Module Type S.
diff --git a/test-suite/output/FunExt.out b/test-suite/output/FunExt.out
index 8d2a125c1d..2a823396d5 100644
--- a/test-suite/output/FunExt.out
+++ b/test-suite/output/FunExt.out
@@ -1,19 +1,12 @@
 The command has indeed failed with message:
-Ltac call to "extensionality in (var)" failed.
 Tactic failure: Not an extensional equality.
 The command has indeed failed with message:
-Ltac call to "extensionality in (var)" failed.
 Tactic failure: Not an extensional equality.
 The command has indeed failed with message:
-Ltac call to "extensionality in (var)" failed.
 Tactic failure: Not an extensional equality.
 The command has indeed failed with message:
-Ltac call to "extensionality in (var)" failed.
 Tactic failure: Not an extensional equality.
 The command has indeed failed with message:
-Ltac call to "extensionality in (var)" failed.
 Tactic failure: Already an intensional equality.
 The command has indeed failed with message:
-In nested Ltac calls to "extensionality in (var)" and
-"clearbody (ne_var_list)", last call failed.
 Hypothesis e depends on the body of H'
diff --git a/test-suite/output/TypeclassDebug.out b/test-suite/output/TypeclassDebug.out
index 8b38fe0ff4..7ea7a08cb3 100644
--- a/test-suite/output/TypeclassDebug.out
+++ b/test-suite/output/TypeclassDebug.out
@@ -14,5 +14,4 @@ Debug: 1.1-1.1-1.1-1.1-1: looking for foo without backtracking
 Debug: 1.1-1.1-1.1-1.1-1.1: simple apply H on foo, 1 subgoal(s)
 Debug: 1.1-1.1-1.1-1.1-1.1-1 : foo
 The command has indeed failed with message:
-Ltac call to "typeclasses eauto (int_or_var_opt) with (ne_preident_list)" failed.
 Tactic failure: Proof search reached its limit.
diff --git a/test-suite/output/bug5778.v b/test-suite/output/bug5778.v
index 0dcd76aeff..441e87af84 100644
--- a/test-suite/output/bug5778.v
+++ b/test-suite/output/bug5778.v
@@ -1,3 +1,4 @@
+Set Ltac Backtrace.
 Ltac a _ := pose (I : I).
 Ltac b _ := a ().
 Ltac abs _ := abstract b ().
diff --git a/test-suite/output/bug6404.v b/test-suite/output/bug6404.v
index bbe6b1a00f..d9e5e20b66 100644
--- a/test-suite/output/bug6404.v
+++ b/test-suite/output/bug6404.v
@@ -1,3 +1,4 @@
+Set Ltac Backtrace.
 Ltac a _ := pose (I : I).
 Ltac b _ := a ().
 Ltac abs _ := transparent_abstract b ().
diff --git a/test-suite/output/ltac.v b/test-suite/output/ltac.v
index 40e743c3f0..fcd5dd05f0 100644
--- a/test-suite/output/ltac.v
+++ b/test-suite/output/ltac.v
@@ -1,3 +1,5 @@
+Set Ltac Backtrace.
+
 (* This used to refer to b instead of z sometimes between 8.4 and 8.5beta3 *)
 Goal True.
 Fail let T := constr:((fun a b : nat => a+b) 1 1) in
diff --git a/test-suite/output/ltac_missing_args.v b/test-suite/output/ltac_missing_args.v
index 91331a1de5..e30c97aac6 100644
--- a/test-suite/output/ltac_missing_args.v
+++ b/test-suite/output/ltac_missing_args.v
@@ -1,3 +1,5 @@
+Set Ltac Backtrace.
+
 Ltac foo x := idtac x.
 Ltac bar x := fun y _ => idtac x y.
 Ltac baz := foo.
diff --git a/test-suite/output/ssr_clear.out b/test-suite/output/ssr_clear.out
index 1515954060..1a0f90493e 100644
--- a/test-suite/output/ssr_clear.out
+++ b/test-suite/output/ssr_clear.out
@@ -1,3 +1,2 @@
 The command has indeed failed with message:
-Ltac call to "move (ssrmovearg) (ssrclauses)" failed.
 No assumption is named NO_SUCH_NAME
diff --git a/test-suite/output/ssr_explain_match.out b/test-suite/output/ssr_explain_match.out
index 32cfb354bf..0f68ab0b02 100644
--- a/test-suite/output/ssr_explain_match.out
+++ b/test-suite/output/ssr_explain_match.out
@@ -51,5 +51,4 @@ instance: (addnC y x) matches: (x + y)
 instance: (addnC y x) matches: (x + y)
 END INSTANCES
 The command has indeed failed with message:
-Ltac call to "ssrinstancesoftpat (cpattern)" failed.
 Not supported