diff options
| -rw-r--r-- | doc/changelog/05-tactic-language/12197-ltacprof-multi-success.rst | 8 | ||||
| -rw-r--r-- | doc/sphinx/proof-engine/ltac.rst | 18 | ||||
| -rw-r--r-- | plugins/ltac/profile_ltac.ml | 92 | ||||
| -rw-r--r-- | test-suite/bugs/closed/bug_12196.v | 46 | ||||
| -rw-r--r-- | test-suite/bugs/closed/bug_6378.v | 9 | ||||
| -rw-r--r-- | test-suite/success/ltacprof.v | 17 |
6 files changed, 132 insertions, 58 deletions
diff --git a/doc/changelog/05-tactic-language/12197-ltacprof-multi-success.rst b/doc/changelog/05-tactic-language/12197-ltacprof-multi-success.rst new file mode 100644 index 0000000000..b90c8e7a1f --- /dev/null +++ b/doc/changelog/05-tactic-language/12197-ltacprof-multi-success.rst @@ -0,0 +1,8 @@ +- **Fixed:** + The :flag:`Ltac Profiling` machinery now correctly handles + backtracking into multi-success tactics. The call-counts of some + tactics are unfortunately inflated by 1, as some tactics are + implicitly implemented as :g:`tac + fail`, which has two + entry-points rather than one (Fixes `#12196 + <https://github.com/coq/coq/issues/12196>`_, `#12197 + <https://github.com/coq/coq/pull/12197>`_, by Jason Gross). diff --git a/doc/sphinx/proof-engine/ltac.rst b/doc/sphinx/proof-engine/ltac.rst index c1eb1f974c..faa44adaf6 100644 --- a/doc/sphinx/proof-engine/ltac.rst +++ b/doc/sphinx/proof-engine/ltac.rst @@ -1778,16 +1778,22 @@ performance issue. and allow displaying and resetting the profile from tactic scripts for benchmarking purposes. +.. warn:: Ltac Profiler encountered an invalid stack (no \ + self node). This can happen if you reset the profile during \ + tactic execution + + Currently, :tacn:`reset ltac profile` is not very well-supported, + as it clears all profiling information about all tactics, including + ones above the current tactic. As a result, the profiler has + trouble understanding where it is in tactic execution. This mixes + especially poorly with backtracking into multi-success tactics. In + general, non-top-level calls to :tacn:`reset ltac profile` should + be avoided. + You can also pass the ``-profile-ltac`` command line option to ``coqc``, which turns the :flag:`Ltac Profiling` flag on at the beginning of each document, and performs a :cmd:`Show Ltac Profile` at the end. -.. warning:: - - Note that the profiler currently does not handle backtracking into - multi-success tactics, and issues a warning to this effect in many cases - when such backtracking occurs. - Run-time optimization tactic ~~~~~~~~~~~~~~~~~~~~~~~~~~~~ diff --git a/plugins/ltac/profile_ltac.ml b/plugins/ltac/profile_ltac.ml index 14fab251d0..c89ecb89bd 100644 --- a/plugins/ltac/profile_ltac.ml +++ b/plugins/ltac/profile_ltac.ml @@ -25,27 +25,20 @@ let is_profiling = Flags.profile_ltac let set_profiling b = is_profiling := b let get_profiling () = !is_profiling -(** 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_profile_backtracking = - CWarnings.create ~name:"profile-backtracking" ~category:"ltac" - (fun () -> strbrk "Ltac Profiler cannot yet handle backtracking \ - into multi-success tactics; profiling results may be wildly inaccurate.") - -let warn_encountered_multi_success_backtracking () = - if !encountered_multi_success_backtracking then - warn_profile_backtracking () - -let encounter_multi_success_backtracking () = - if not !encountered_multi_success_backtracking +let encountered_invalid_stack_no_self = ref false + +let warn_invalid_stack_no_self = + CWarnings.create ~name:"profile-invalid-stack-no-self" ~category:"ltac" + (fun () -> strbrk + "Ltac Profiler encountered an invalid stack (no self \ + node). This can happen if you reset the profile during \ + tactic execution.") + +let encounter_invalid_stack_no_self () = + if not !encountered_invalid_stack_no_self then begin - encountered_multi_success_backtracking := true; - warn_encountered_multi_success_backtracking () + encountered_invalid_stack_no_self := true; + warn_invalid_stack_no_self () end @@ -76,8 +69,7 @@ module Local = Summary.Local let stack = Local.ref ~name:"LtacProf-stack" [empty_treenode root] let reset_profile_tmp () = - Local.(stack := [empty_treenode root]); - encountered_multi_success_backtracking := false + Local.(stack := [empty_treenode root]) (* ************** XML Serialization ********************* *) @@ -218,7 +210,6 @@ let to_string ~filter ?(cutoff=0.0) node = cumulate tree; !global in - warn_encountered_multi_success_backtracking (); let filter s n = filter s && (all_total <= 0.0 || n /. all_total >= cutoff /. 100.0) in let msg = h 0 (str "total time: " ++ padl 11 (format_sec (all_total))) ++ @@ -296,13 +287,15 @@ let exit_tactic ~count_call start_time c = match Local.(!stack) with | [] | [_] -> (* oops, our stack is invalid *) - encounter_multi_success_backtracking (); + encounter_invalid_stack_no_self (); reset_profile_tmp () | node :: (parent :: rest as full_stack) -> let name = string_of_call c in if not (String.equal name node.name) then (* oops, our stack is invalid *) - encounter_multi_success_backtracking (); + CErrors.anomaly + (Pp.strbrk "Ltac Profiler encountered an invalid stack (wrong self node) \ + likely due to backtracking into multi-success tactics."); let node = { node with total = node.total +. diff; local = node.local +. diff; @@ -332,38 +325,32 @@ let exit_tactic ~count_call start_time c = (* Calls are over, we reset the stack and send back data *) if rest == [] && get_profiling () then begin assert(String.equal root parent.name); + encountered_invalid_stack_no_self := false; reset_profile_tmp (); feedback_results parent end -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 ?(count_call=true) tac = - let open Proofview.Notations in - Proofview.tclLIFT (Proofview.NonLogical.make (fun () -> - if !is_profiling then - match call_trace, Local.(!stack) with - | (_, c) :: _, parent :: rest -> - let name = string_of_call c in - let node = get_child name parent in - Local.(stack := node :: parent :: rest); - Some (time ()) - | _ :: _, [] -> assert false - | _ -> None - else None)) >>= function - | Some start_time -> - tclFINALLY - tac - (Proofview.tclLIFT (Proofview.NonLogical.make (fun () -> - (match call_trace with - | (_, c) :: _ -> exit_tactic ~count_call start_time c - | [] -> ())))) - | None -> tac + Proofview.tclWRAPFINALLY + (Proofview.tclLIFT (Proofview.NonLogical.make (fun () -> + if !is_profiling then + match call_trace, Local.(!stack) with + | (_, c) :: _, parent :: rest -> + let name = string_of_call c in + let node = get_child name parent in + Local.(stack := node :: parent :: rest); + Some (time ()) + | _ :: _, [] -> assert false + | _ -> None + else None))) + tac + (function + | Some start_time -> + (Proofview.tclLIFT (Proofview.NonLogical.make (fun () -> + (match call_trace with + | (_, c) :: _ -> exit_tactic ~count_call start_time c + | [] -> ())))) + | None -> Proofview.tclUNIT ()) (* ************** Accumulation of data from workers ************************* *) @@ -396,6 +383,7 @@ let _ = | _ -> ())) let reset_profile () = + encountered_invalid_stack_no_self := false; reset_profile_tmp (); data := SM.empty diff --git a/test-suite/bugs/closed/bug_12196.v b/test-suite/bugs/closed/bug_12196.v new file mode 100644 index 0000000000..c0851b3204 --- /dev/null +++ b/test-suite/bugs/closed/bug_12196.v @@ -0,0 +1,46 @@ +(** TODO: Figure out how to test "sanity" for the ltac profiler output *) +Fixpoint fact (n : nat) := match n with 0 => 1 | S n' => n * fact n' end. +Fixpoint walk (n : nat) := match n with 0 => tt | S n => walk n end. +Ltac slow := idtac + (do 2 (let x := eval lazy in (walk (fact 9)) in idtac)). +Ltac slow2 := idtac + (do 2 (let x := eval lazy in (walk (fact 9)) in idtac)). +Ltac multi := idtac + slow + slow2. +Set Ltac Profiling. +Goal True. + Time try (multi; fail). + (* Warning: Ltac Profiler cannot yet handle backtracking into multi-success + tactics; profiling results may be wildly inaccurate. + [profile-backtracking,ltac] *) + Show Ltac Profile. + (* Used to be: +total time: 0.000s + + tactic local total calls max +────────────────────────────────────────┴──────┴──────┴───────┴─────────┘ +─multi --------------------------------- 47.1% 47.1% 1 0.000s +─slow ---------------------------------- 35.3% 35.3% 1 0.000s +─slow2 --------------------------------- 17.6% 17.6% 1 0.000s + + tactic local total calls max +────────────────────────────────────────┴──────┴──────┴───────┴─────────┘ +─multi --------------------------------- 47.1% 47.1% 1 0.000s +─slow ---------------------------------- 35.3% 35.3% 1 0.000s +─slow2 --------------------------------- 17.6% 17.6% 1 0.000s + + *) + (* Now: +total time: 2.074s + + tactic local total calls max +────────────────────────────────────────┴──────┴──────┴───────┴─────────┘ +─multi --------------------------------- 0.0% 100.0% 6 1.119s +─slow ---------------------------------- 54.0% 54.0% 3 1.119s +─slow2 --------------------------------- 46.0% 46.0% 3 0.955s + + tactic local total calls max +────────────────────────────────────────┴──────┴──────┴───────┴─────────┘ +─multi --------------------------------- 0.0% 100.0% 6 1.119s + ├─slow -------------------------------- 54.0% 54.0% 3 1.119s + └─slow2 ------------------------------- 46.0% 46.0% 3 0.955s + +*) +Abort. diff --git a/test-suite/bugs/closed/bug_6378.v b/test-suite/bugs/closed/bug_6378.v index 68ae7961dd..453924d587 100644 --- a/test-suite/bugs/closed/bug_6378.v +++ b/test-suite/bugs/closed/bug_6378.v @@ -7,11 +7,20 @@ Ltac profile_constr tac := Ltac slow _ := eval vm_compute in (Z.div_eucl, Z.div_eucl, Z.div_eucl, Z.div_eucl, Z.div_eucl). +Ltac manipulate_ltac_prof := + start ltac profiling; + reset ltac profile; + try ((idtac + reset ltac profile + idtac); fail); + try ((idtac + start ltac profiling + idtac); fail); + try ((idtac + stop ltac profiling + idtac); fail). + Goal True. start ltac profiling. reset ltac profile. + manipulate_ltac_prof. reset ltac profile. stop ltac profiling. + Set Warnings Append "+profile-invalid-stack-no-self". time profile_constr slow. show ltac profile cutoff 0. show ltac profile "slow". diff --git a/test-suite/success/ltacprof.v b/test-suite/success/ltacprof.v index d5552695c4..f40f40c2bb 100644 --- a/test-suite/success/ltacprof.v +++ b/test-suite/success/ltacprof.v @@ -6,3 +6,20 @@ Goal True. try (multi; fail). (* Used to result in: Anomaly: Uncaught exception Failure("hd"). Please report. *) Admitted. Show Ltac Profile. + +(* backtracking across profiler manipulation *) +Unset Ltac Profiling. +Reset Ltac Profile. + +Fixpoint slow (n : nat) : unit + := match n with + | 0 => tt + | S n => fst (slow n, slow n) + end. + +Ltac slow := idtac; let v := eval cbv in (slow 16) in idtac. +Ltac multi2 := + try (((idtac; slow) + (start ltac profiling; slow) + (idtac; slow) + (slow; stop ltac profiling; slow) + slow + (start ltac profiling; (idtac + slow); ((stop ltac profiling + idtac); fail))); slow; fail); slow; show ltac profile. +Goal True. + multi2. +Admitted. |