aboutsummaryrefslogtreecommitdiff
path: root/ltac
diff options
context:
space:
mode:
Diffstat (limited to 'ltac')
-rw-r--r--ltac/ltac.mllib2
-rw-r--r--ltac/profile_ltac.ml323
-rw-r--r--ltac/profile_ltac.mli25
-rw-r--r--ltac/profile_ltac_tactics.ml439
-rw-r--r--ltac/tacintern.ml18
-rw-r--r--ltac/tacinterp.ml43
-rw-r--r--ltac/tactic_debug.ml21
7 files changed, 437 insertions, 34 deletions
diff --git a/ltac/ltac.mllib b/ltac/ltac.mllib
index e0c6f3ac0a..65ed114cff 100644
--- a/ltac/ltac.mllib
+++ b/ltac/ltac.mllib
@@ -3,6 +3,7 @@ Tacenv
Tactic_debug
Tacintern
Tacentries
+Profile_ltac
Tacinterp
Evar_tactics
Tactic_option
@@ -10,6 +11,7 @@ Extraargs
G_obligations
Coretactics
Extratactics
+Profile_ltac_tactics
G_auto
G_class
Rewrite
diff --git a/ltac/profile_ltac.ml b/ltac/profile_ltac.ml
new file mode 100644
index 0000000000..7a8ef32c3f
--- /dev/null
+++ b/ltac/profile_ltac.ml
@@ -0,0 +1,323 @@
+(************************************************************************)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
+(* \VV/ **************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(************************************************************************)
+
+open Unicode
+open Pp
+open Printer
+open Util
+
+(** [is_profiling] and the profiling info ([stack]) should be synchronized with
+ the document; the rest of the ref cells are either local to individual
+ tactic invocations, or global flags, and need not be synchronized, since no
+ document-level backtracking happens within tactics. We synchronize
+ is_profiling via an option. *)
+let is_profiling = Flags.profile_ltac
+
+let set_profiling b = is_profiling := b
+let get_profiling () = !is_profiling
+
+let new_call = ref false
+let entered_call () = new_call := true
+let is_new_call () = let b = !new_call in new_call := false; b
+
+(** LtacProf cannot yet handle backtracking into multi-success tactics.
+ To properly support this, we'd have to somehow recreate our location in the
+ call-stack, and stop/restart the intervening timers. This is tricky and
+ possibly expensive, so instead we currently just emit a warning that
+ profiling results will be off. *)
+let encountered_multi_success_backtracking = ref false
+
+let warn_encountered_multi_success_backtracking () =
+ if !encountered_multi_success_backtracking then
+ Feedback.msg_warning (str "Ltac Profiler cannot yet handle backtracking \
+ into multi-success tactics; profiling results may be wildly inaccurate.")
+
+let encounter_multi_success_backtracking () =
+ if not !encountered_multi_success_backtracking
+ then begin
+ encountered_multi_success_backtracking := true;
+ warn_encountered_multi_success_backtracking ()
+ end
+
+type entry = {
+ mutable total : float;
+ mutable local : float;
+ mutable ncalls : int;
+ mutable max_total : float
+}
+
+let empty_entry () = { total = 0.; local = 0.; ncalls = 0; max_total = 0. }
+
+let add_entry e add_total { total; local; ncalls; max_total } =
+ if add_total then e.total <- e.total +. total;
+ e.local <- e.local +. local;
+ e.ncalls <- e.ncalls + ncalls;
+ if add_total then e.max_total <- max e.max_total max_total
+
+type treenode = {
+ entry : entry;
+ children : (string, treenode) Hashtbl.t
+}
+
+let empty_treenode n = { entry = empty_entry (); children = Hashtbl.create n }
+
+(** Tobias Tebbi wrote some tricky code involving mutation. Rather than
+ rewriting it in a functional style, we simply freeze the state when we need
+ to by issuing a deep copy of the profiling data. *)
+(** TODO: rewrite me in purely functional style *)
+let deepcopy_entry { total; local; ncalls; max_total } =
+ { total; local; ncalls; max_total }
+
+let rec deepcopy_treenode { entry; children } =
+ let children' = Hashtbl.create (Hashtbl.length children) in
+ let iter key subtree = Hashtbl.add children' key (deepcopy_treenode subtree) in
+ let () = Hashtbl.iter iter children in
+ { entry = deepcopy_entry entry; children = children' }
+
+let stack =
+ let freeze _ = List.map deepcopy_treenode in
+ Summary.ref ~freeze [empty_treenode 20] ~name:"LtacProf-stack"
+
+let on_stack = Hashtbl.create 5
+
+let get_node c table =
+ try Hashtbl.find table c
+ with Not_found ->
+ let new_node = empty_treenode 5 in
+ Hashtbl.add table c new_node;
+ new_node
+
+let rec add_node node node' =
+ add_entry node.entry true node'.entry;
+ Hashtbl.iter
+ (fun s node' -> add_node (get_node s node.children) node')
+ node'.children
+
+let time () =
+ let times = Unix.times () in
+ times.Unix.tms_utime +. times.Unix.tms_stime
+
+(*
+let msgnl_with fmt strm = msg_with fmt (strm ++ fnl ())
+let msgnl strm = msgnl_with !Pp_control.std_ft strm
+
+let rec print_treenode indent (tn : treenode) =
+ msgnl (str (indent^"{ entry = {"));
+ Feedback.msg_notice (str (indent^"total = "));
+ msgnl (str (indent^(string_of_float (tn.entry.total))));
+ Feedback.msg_notice (str (indent^"local = "));
+ msgnl (str (indent^(string_of_float tn.entry.local)));
+ Feedback.msg_notice (str (indent^"ncalls = "));
+ msgnl (str (indent^(string_of_int tn.entry.ncalls)));
+ Feedback.msg_notice (str (indent^"max_total = "));
+ msgnl (str (indent^(string_of_float tn.entry.max_total)));
+ msgnl (str (indent^"}"));
+ msgnl (str (indent^"children = {"));
+ Hashtbl.iter
+ (fun s node ->
+ msgnl (str (indent^" "^s^" |-> "));
+ print_treenode (indent^" ") node
+ )
+ tn.children;
+ msgnl (str (indent^"} }"))
+
+let rec print_stack (st : treenode list) = match st with
+| [] -> msgnl (str "[]")
+| x :: xs -> print_treenode "" x; msgnl (str ("::")); print_stack xs
+*)
+
+let string_of_call ck =
+ let s =
+ string_of_ppcmds
+ (match ck with
+ | Tacexpr.LtacNotationCall s -> Names.KerName.print s
+ | Tacexpr.LtacNameCall cst -> Pptactic.pr_ltac_constant cst
+ | Tacexpr.LtacVarCall (id, t) -> Nameops.pr_id id
+ | Tacexpr.LtacAtomCall te ->
+ (Pptactic.pr_glob_tactic (Global.env ())
+ (Tacexpr.TacAtom (Loc.ghost, te)))
+ | Tacexpr.LtacConstrInterp (c, _) ->
+ pr_glob_constr_env (Global.env ()) c
+ | Tacexpr.LtacMLCall te ->
+ (Pptactic.pr_glob_tactic (Global.env ())
+ te)
+ ) in
+ for i = 0 to String.length s - 1 do if s.[i] = '\n' then s.[i] <- ' ' done;
+ let s = try String.sub s 0 (CString.string_index_from s 0 "(*") with Not_found -> s in
+ CString.strip s
+
+let exit_tactic start_time add_total c = match !stack with
+| [] | [_] ->
+ (* oops, our stack is invalid *)
+ encounter_multi_success_backtracking ()
+| node :: (parent :: _ as stack') ->
+ stack := stack';
+ if add_total then Hashtbl.remove on_stack (string_of_call c);
+ let diff = time () -. start_time in
+ parent.entry.local <- parent.entry.local -. diff;
+ let node' = { total = diff; local = diff; ncalls = 1; max_total = diff } in
+ add_entry node.entry add_total node'
+
+let tclFINALLY tac (finally : unit Proofview.tactic) =
+ let open Proofview.Notations in
+ Proofview.tclIFCATCH
+ tac
+ (fun v -> finally <*> Proofview.tclUNIT v)
+ (fun (exn, info) -> finally <*> Proofview.tclZERO ~info exn)
+
+let do_profile s call_trace tac =
+ let open Proofview.Notations in
+ Proofview.tclLIFT (Proofview.NonLogical.make (fun () ->
+ if !is_profiling && is_new_call () then
+ match call_trace with
+ | (_, c) :: _ ->
+ let s = string_of_call c in
+ let parent = List.hd !stack in
+ let node, add_total = try Hashtbl.find on_stack s, false
+ with Not_found ->
+ let node = get_node s parent.children in
+ Hashtbl.add on_stack s node;
+ node, true
+ in
+ if not add_total && node = List.hd !stack then None else (
+ stack := node :: !stack;
+ let start_time = time () in
+ Some (start_time, add_total)
+ )
+ | [] -> None
+ else None)) >>= function
+ | Some (start_time, add_total) ->
+ tclFINALLY
+ tac
+ (Proofview.tclLIFT (Proofview.NonLogical.make (fun () ->
+ (match call_trace with
+ | (_, c) :: _ ->
+ exit_tactic start_time add_total c
+ | [] -> ()))))
+ | None -> tac
+
+
+
+let format_sec x = (Printf.sprintf "%.3fs" x)
+let format_ratio x = (Printf.sprintf "%.1f%%" (100. *. x))
+let padl n s = ws (max 0 (n - utf8_length s)) ++ str s
+let padr n s = str s ++ ws (max 0 (n - utf8_length s))
+let padr_with c n s =
+ let ulength = utf8_length s in
+ str (utf8_sub s 0 n) ++ str (String.make (max 0 (n - ulength)) c)
+
+let rec list_iter_is_last f = function
+ | [] -> []
+ | [x] -> [f true x]
+ | x :: xs -> f false x :: list_iter_is_last f xs
+
+let header =
+ str " tactic self total calls max" ++
+ fnl () ++
+ str "────────────────────────────────────────┴──────┴──────┴───────┴─────────┘"
+
+let rec print_node all_total indent prefix (s, n) =
+ let e = n.entry in
+ h 0 (
+ padr_with '-' 40 (prefix ^ s ^ " ")
+ ++ padl 7 (format_ratio (e.local /. all_total))
+ ++ padl 7 (format_ratio (e.total /. all_total))
+ ++ padl 8 (string_of_int e.ncalls)
+ ++ padl 10 (format_sec (e.max_total))
+ ) ++
+ print_table all_total indent false n.children
+
+and print_table all_total indent first_level table =
+ let fold s n l = if n.entry.total /. all_total < 0.02 then l else (s, n) :: l in
+ let ls = Hashtbl.fold fold table [] in
+ match ls with
+ | [s, n] when not first_level ->
+ print_node all_total indent (indent ^ "└") (s, n)
+ | _ ->
+ let ls = List.sort (fun (_, n1) (_, n2) -> compare n2.entry.total n1.entry.total) ls in
+ let iter is_last =
+ let sep0 = if first_level then "" else if is_last then " " else " │" in
+ let sep1 = if first_level then "─" else if is_last then " └─" else " ├─" in
+ print_node all_total (indent ^ sep0) (indent ^ sep1)
+ in
+ prlist_with_sep fnl (fun pr -> pr) (list_iter_is_last iter ls)
+
+let print_results () =
+ let tree = (List.hd !stack).children in
+ let all_total = -. (List.hd !stack).entry.local in
+ let global = Hashtbl.create 20 in
+ let rec cumulate table =
+ let iter s node =
+ let node' = get_node s global in
+ add_entry node'.entry true node.entry;
+ cumulate node.children
+ in
+ Hashtbl.iter iter table
+ in
+ cumulate tree;
+ warn_encountered_multi_success_backtracking ();
+ let msg =
+ h 0 (str "total time: " ++ padl 11 (format_sec (all_total))) ++
+ fnl () ++
+ header ++
+ print_table all_total "" true global ++
+ fnl () ++
+ header ++
+ print_table all_total "" true tree
+ in
+ Feedback.msg_notice msg
+ (* FOR DEBUGGING *)
+ (* ;
+ msgnl (str"");
+ print_stack (!stack)
+ *)
+
+let print_results_tactic tactic =
+ let tree = (List.hd !stack).children in
+ let table_tactic = Hashtbl.create 20 in
+ let rec cumulate table =
+ let iter s node =
+ if String.sub (s ^ ".") 0 (min (1 + String.length s) (String.length tactic)) = tactic
+ then add_node (get_node s table_tactic) node
+ else cumulate node.children
+ in
+ Hashtbl.iter iter table
+ in
+ cumulate tree;
+ let all_total = -. (List.hd !stack).entry.local in
+ let tactic_total =
+ Hashtbl.fold
+ (fun _ node all_total -> node.entry.total +. all_total)
+ table_tactic 0. in
+ warn_encountered_multi_success_backtracking ();
+ let msg =
+ h 0 (str"total time: " ++ padl 11 (format_sec (all_total))) ++
+ h 0 (str"time spent in tactic: " ++ padl 11 (format_sec (tactic_total))) ++
+ fnl () ++
+ header ++
+ print_table tactic_total "" true table_tactic
+ in
+ Feedback.msg_notice msg
+
+let reset_profile () =
+ stack := [empty_treenode 20];
+ encountered_multi_success_backtracking := false
+
+let do_print_results_at_close () = if get_profiling () then print_results ()
+
+let _ = Declaremods.append_end_library_hook do_print_results_at_close
+
+let _ =
+ let open Goptions in
+ declare_bool_option
+ { optsync = true;
+ optdepr = false;
+ optname = "Ltac Profiling";
+ optkey = ["Ltac"; "Profiling"];
+ optread = get_profiling;
+ optwrite = set_profiling }
diff --git a/ltac/profile_ltac.mli b/ltac/profile_ltac.mli
new file mode 100644
index 0000000000..7bbdca9425
--- /dev/null
+++ b/ltac/profile_ltac.mli
@@ -0,0 +1,25 @@
+(************************************************************************)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
+(* \VV/ **************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(************************************************************************)
+
+(** Ltac profiling primitives *)
+
+val do_profile : string -> ('a * Tacexpr.ltac_call_kind) list -> 'b Proofview.tactic -> 'b Proofview.tactic
+
+val set_profiling : bool -> unit
+
+val get_profiling : unit -> bool
+
+val entered_call : unit -> unit
+
+val print_results : unit -> unit
+
+val print_results_tactic : string -> unit
+
+val reset_profile : unit -> unit
+
+val do_print_results_at_close : unit -> unit
diff --git a/ltac/profile_ltac_tactics.ml4 b/ltac/profile_ltac_tactics.ml4
new file mode 100644
index 0000000000..c092a0cb61
--- /dev/null
+++ b/ltac/profile_ltac_tactics.ml4
@@ -0,0 +1,39 @@
+(************************************************************************)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
+(* \VV/ **************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(************************************************************************)
+
+(*i camlp4deps: "grammar/grammar.cma" i*)
+
+(** Ltac profiling entrypoints *)
+
+open Profile_ltac
+open Stdarg
+
+DECLARE PLUGIN "profile_ltac_plugin"
+
+let tclSET_PROFILING b =
+ Proofview.tclLIFT (Proofview.NonLogical.make (fun () -> set_profiling b))
+
+TACTIC EXTEND start_ltac_profiling
+| [ "start" "ltac" "profiling" ] -> [ tclSET_PROFILING true ]
+END
+
+TACTIC EXTEND stop_profiling
+| [ "stop" "ltac" "profiling" ] -> [ tclSET_PROFILING false ]
+END
+
+VERNAC COMMAND EXTEND ResetLtacProfiling CLASSIFIED AS SIDEFF
+ [ "Reset" "Ltac" "Profile" ] -> [ reset_profile() ]
+END
+
+VERNAC COMMAND EXTEND ShowLtacProfile CLASSIFIED AS QUERY
+ [ "Show" "Ltac" "Profile" ] -> [ print_results() ]
+END
+
+VERNAC COMMAND EXTEND ShowLtacProfileTactic CLASSIFIED AS QUERY
+ [ "Show" "Ltac" "Profile" string(s) ] -> [ print_results_tactic s ]
+END
diff --git a/ltac/tacintern.ml b/ltac/tacintern.ml
index d39f835528..7cda7d1377 100644
--- a/ltac/tacintern.ml
+++ b/ltac/tacintern.ml
@@ -424,7 +424,7 @@ let intern_hyp_location ist ((occs,id),hl) =
(* Reads a pattern *)
let intern_pattern ist ?(as_type=false) ltacvars = function
| Subterm (b,ido,pc) ->
- let (metas,pc) = intern_constr_pattern ist ~as_type ~ltacvars pc in
+ let (metas,pc) = intern_constr_pattern ist ~as_type:false ~ltacvars pc in
ido, metas, Subterm (b,ido,pc)
| Term pc ->
let (metas,pc) = intern_constr_pattern ist ~as_type ~ltacvars pc in
@@ -446,7 +446,7 @@ let opt_cons accu = function
| Some id -> Id.Set.add id accu
(* Reads the hypotheses of a "match goal" rule *)
-let rec intern_match_goal_hyps ist lfun = function
+let rec intern_match_goal_hyps ist ?(as_type=false) lfun = function
| (Hyp ((_,na) as locna,mp))::tl ->
let ido, metas1, pat = intern_pattern ist ~as_type:true lfun mp in
let lfun, metas2, hyps = intern_match_goal_hyps ist lfun tl in
@@ -455,7 +455,7 @@ let rec intern_match_goal_hyps ist lfun = function
| (Def ((_,na) as locna,mv,mp))::tl ->
let ido, metas1, patv = intern_pattern ist ~as_type:false lfun mv in
let ido', metas2, patt = intern_pattern ist ~as_type:true lfun mp in
- let lfun, metas3, hyps = intern_match_goal_hyps ist lfun tl in
+ let lfun, metas3, hyps = intern_match_goal_hyps ist ~as_type lfun tl in
let lfun' = name_cons (opt_cons (opt_cons lfun ido) ido') na in
lfun', metas1@metas2@metas3, Def (locna,patv,patt)::hyps
| [] -> lfun, [], []
@@ -564,7 +564,7 @@ and intern_tactic_seq onlytac ist = function
ist.ltacvars, TacLetIn (isrec,l,intern_tactic onlytac ist' u)
| TacMatchGoal (lz,lr,lmr) ->
- ist.ltacvars, (TacMatchGoal(lz,lr, intern_match_rule onlytac ist lmr))
+ ist.ltacvars, (TacMatchGoal(lz,lr, intern_match_rule onlytac ist ~as_type:true lmr))
| TacMatch (lz,c,lmr) ->
ist.ltacvars,
TacMatch (lz,intern_tactic_or_tacarg ist c,intern_match_rule onlytac ist lmr)
@@ -666,18 +666,18 @@ and intern_tacarg strict onlytac ist = function
TacGeneric arg
(* Reads the rules of a Match Context or a Match *)
-and intern_match_rule onlytac ist = function
+and intern_match_rule onlytac ist ?(as_type=false) = function
| (All tc)::tl ->
- All (intern_tactic onlytac ist tc) :: (intern_match_rule onlytac ist tl)
+ All (intern_tactic onlytac ist tc) :: (intern_match_rule onlytac ist ~as_type tl)
| (Pat (rl,mp,tc))::tl ->
let {ltacvars=lfun; genv=env} = ist in
- let lfun',metas1,hyps = intern_match_goal_hyps ist lfun rl in
- let ido,metas2,pat = intern_pattern ist lfun mp in
+ let lfun',metas1,hyps = intern_match_goal_hyps ist ~as_type lfun rl in
+ let ido,metas2,pat = intern_pattern ist ~as_type lfun mp in
let fold accu x = Id.Set.add x accu in
let ltacvars = List.fold_left fold (opt_cons lfun' ido) metas1 in
let ltacvars = List.fold_left fold ltacvars metas2 in
let ist' = { ist with ltacvars } in
- Pat (hyps,pat,intern_tactic onlytac ist' tc) :: (intern_match_rule onlytac ist tl)
+ Pat (hyps,pat,intern_tactic onlytac ist' tc) :: (intern_match_rule onlytac ist ~as_type tl)
| [] -> []
and intern_genarg ist (GenArg (Rawwit wit, x)) =
diff --git a/ltac/tacinterp.ml b/ltac/tacinterp.ml
index 5ee9b0fc4d..ab61c8abba 100644
--- a/ltac/tacinterp.ml
+++ b/ltac/tacinterp.ml
@@ -286,9 +286,10 @@ 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 -> [call]
-| Some trace -> call :: trace
+| None -> Proofview.tclUNIT [call]
+| Some trace -> Proofview.tclLIFT (Proofview.NonLogical.make Profile_ltac.entered_call) <*> Proofview.tclUNIT (call :: trace)
let propagate_trace ist loc id v =
let v = Value.normalize v in
@@ -297,10 +298,11 @@ let propagate_trace ist loc id v =
match tacv with
| VFun (appl,_,lfun,it,b) ->
let t = if List.is_empty it then b else TacFun (it,b) in
- let ans = VFun (appl,push_trace(loc,LtacVarCall (id,t)) ist,lfun,it,b) in
- of_tacvalue ans
- | _ -> v
- else v
+ push_trace(loc,LtacVarCall (id,t)) ist >>= fun trace ->
+ let ans = VFun (appl,trace,lfun,it,b) in
+ Proofview.tclUNIT (of_tacvalue ans)
+ | _ -> Proofview.tclUNIT v
+ else Proofview.tclUNIT v
let append_trace trace v =
let v = Value.normalize v in
@@ -622,8 +624,13 @@ let interp_gen kind ist allow_patvar flags env sigma (c,ce) =
match kind with OfType _ -> WithoutTypeConstraint | _ -> kind in
intern_gen kind_for_intern ~allow_patvar ~ltacvars env c
in
- let trace =
- push_trace (loc_of_glob_constr c,LtacConstrInterp (c,vars)) ist in
+ (* Jason Gross: To avoid unnecessary modifications to tacinterp, as
+ suggested by Arnaud Spiwack, we run push_trace immediately. We do
+ this with the kludge of an empty proofview, and rely on the
+ invariant that running the tactic returned by push_trace does
+ not modify sigma. *)
+ let (_, dummy_proofview) = Proofview.init sigma [] in
+ let (trace,_,_,_) = Proofview.apply env (push_trace (loc_of_glob_constr c,LtacConstrInterp (c,vars)) ist) dummy_proofview in
let (evd,c) =
catch_error trace (understand_ltac flags env sigma vars kind) c
in
@@ -1169,7 +1176,9 @@ let rec val_interp ist ?(appl=UnnamedAppl) (tac:glob_tactic_expr) : Val.t Ftacti
and eval_tactic ist tac : unit Proofview.tactic = match tac with
| TacAtom (loc,t) ->
let call = LtacAtomCall t in
- catch_error_tac (push_trace(loc,call) ist) (interp_atomic ist t)
+ push_trace(loc,call) ist >>= fun trace ->
+ Profile_ltac.do_profile "eval_tactic:2" trace
+ (catch_error_tac trace (interp_atomic ist t))
| TacFun _ | TacLetIn _ -> assert false
| TacMatchGoal _ | TacMatch _ -> assert false
| TacId [] -> Proofview.tclLIFT (db_breakpoint (curr_debug ist) [])
@@ -1251,7 +1260,7 @@ and eval_tactic ist tac : unit Proofview.tactic = match tac with
let tac l =
let addvar x v accu = Id.Map.add x v accu in
let lfun = List.fold_right2 addvar ids l ist.lfun in
- let trace = push_trace (loc,LtacNotationCall s) ist in
+ Ftactic.lift (push_trace (loc,LtacNotationCall s) ist) >>= fun trace ->
let ist = {
lfun = lfun;
extra = TacStore.set ist.extra f_trace trace; } in
@@ -1276,7 +1285,7 @@ and eval_tactic ist tac : unit Proofview.tactic = match tac with
Ftactic.run tac (fun () -> Proofview.tclUNIT ())
| TacML (loc,opn,l) ->
- let trace = push_trace (loc,LtacMLCall tac) ist in
+ push_trace (loc,LtacMLCall tac) ist >>= fun trace ->
let ist = { ist with extra = TacStore.set ist.extra f_trace trace; } in
let tac = Tacenv.interp_ml_tactic opn in
let args = Ftactic.List.map_right (fun a -> interp_tacarg ist a) l in
@@ -1302,15 +1311,17 @@ and interp_ltac_reference loc' mustbetac ist r : Val.t Ftactic.t =
try Id.Map.find id ist.lfun
with Not_found -> in_gen (topwit wit_var) id
in
- Ftactic.bind (force_vrec ist v) begin fun v ->
- let v = propagate_trace ist loc id v in
+ let open Ftactic in
+ force_vrec ist v >>= begin fun v ->
+ Ftactic.lift (propagate_trace ist loc id v) >>= fun v ->
if mustbetac then Ftactic.return (coerce_to_tactic loc id v) else Ftactic.return v
end
| ArgArg (loc,r) ->
let ids = extract_ids [] ist.lfun in
let loc_info = ((if Loc.is_ghost loc' then loc else loc'),LtacNameCall r) in
- let extra = TacStore.set ist.extra f_avoid_ids ids in
- let extra = TacStore.set extra f_trace (push_trace loc_info ist) in
+ let extra = TacStore.set ist.extra f_avoid_ids ids in
+ push_trace loc_info ist >>= fun trace ->
+ let extra = TacStore.set extra f_trace trace in
let ist = { lfun = Id.Map.empty; extra = extra; } in
let appl = GlbAppl[r,[]] in
val_interp ~appl ist (Tacenv.interp_ltac r)
@@ -1408,7 +1419,7 @@ and tactic_of_value ist vle =
lfun = lfun;
extra = TacStore.set ist.extra f_trace []; } in
let tac = name_if_glob appl (eval_tactic ist t) in
- catch_error_tac trace tac
+ Profile_ltac.do_profile "tactic_of_value" trace (catch_error_tac trace tac)
| (VFun _|VRec _) -> Tacticals.New.tclZEROMSG (str "A fully applied tactic is expected.")
else if has_type vle (topwit wit_tactic) then
let tac = out_gen (topwit wit_tactic) vle in
diff --git a/ltac/tactic_debug.ml b/ltac/tactic_debug.ml
index d661f9677c..e657eb9bc2 100644
--- a/ltac/tactic_debug.ml
+++ b/ltac/tactic_debug.ml
@@ -330,10 +330,9 @@ let db_breakpoint debug s =
let is_defined_ltac trace =
let rec aux = function
- | (_, Tacexpr.LtacNameCall f) :: tail ->
- not (Tacenv.is_ltac_for_ml_tactic f)
- | (_, Tacexpr.LtacAtomCall _) :: tail ->
- false
+ | (_, Tacexpr.LtacNameCall f) :: _ -> not (Tacenv.is_ltac_for_ml_tactic f)
+ | (_, Tacexpr.LtacNotationCall f) :: _ -> true
+ | (_, Tacexpr.LtacAtomCall _) :: _ -> false
| _ :: tail -> aux tail
| [] -> false in
aux (List.rev trace)
@@ -341,7 +340,7 @@ let is_defined_ltac trace =
let explain_ltac_call_trace last trace loc =
let calls = last :: List.rev_map snd trace in
let pr_call ck = match ck with
- | Tacexpr.LtacNotationCall kn -> quote (KerName.print kn)
+ | Tacexpr.LtacNotationCall kn -> quote (Pptactic.pr_alias_key kn)
| Tacexpr.LtacNameCall cst -> quote (Pptactic.pr_ltac_constant cst)
| Tacexpr.LtacMLCall t ->
quote (Pptactic.pr_glob_tactic (Global.env()) t)
@@ -363,6 +362,7 @@ let explain_ltac_call_trace last trace loc =
in
match calls with
| [] -> mt ()
+ | [a] -> hov 0 (str "Ltac call to " ++ pr_call a ++ str " failed.")
| _ ->
let kind_of_last_call = match List.last calls with
| Tacexpr.LtacConstrInterp _ -> ", last term evaluation failed."
@@ -373,10 +373,13 @@ let explain_ltac_call_trace last trace loc =
let skip_extensions trace =
let rec aux = function
- | (_,Tacexpr.LtacNameCall f as tac) :: _
- when Tacenv.is_ltac_for_ml_tactic f -> [tac]
- | (_,(Tacexpr.LtacNotationCall _ | Tacexpr.LtacMLCall _) as tac)
- :: _ -> [tac]
+ | (_,Tacexpr.LtacNameCall f as tac) :: _
+ when Tacenv.is_ltac_for_ml_tactic f -> [tac]
+ | (_,Tacexpr.LtacNotationCall _ as tac) :: (_,Tacexpr.LtacMLCall _) :: _ ->
+ (* Case of an ML defined tactic with entry of the form <<"foo" args>> *)
+ (* see tacextend.mlp *)
+ [tac]
+ | (_,Tacexpr.LtacMLCall _ as tac) :: _ -> [tac]
| t :: tail -> t :: aux tail
| [] -> [] in
List.rev (aux (List.rev trace))
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-01 04:51:48 +0000