From 1700c63e82c0b10cbdeda8d79639d925a7571e12 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Tue, 28 Apr 2020 14:44:37 -0400 Subject: Add Proofview.tclWRAPFINALLY This new primitive (which could be implemented in terms of `tclCASE`, but which I believe encapsulates a useful unit of behavior) is needed for correctly implementing both `with_strategy` and for implementing multi-success support for the Ltac Profiler. The basic function of this tactical is to allow wrapping multi-success tactics with initialization and cleanup routines. For example, if `tac` is a multi-success tactic that writes its status to a log file, you might want to wrap `tac` in "first open the log file" and then after it runs "finally close the log file". (Unfortunately, the way the monad is set up doesn't allow passing data from the most recent run of the initializer to the tactic, which suggests that perhaps there's something a bit off about this abstraction. Perhaps we should set up a ref cell and that will hold the most recent return of the initializer and pass this ref cell to the wrapped tactic? But this can be done externally without needing to modify the current API. In any case, such data is not needed in the case of the Ltac Profiler, where the initializer is "update the current call stack and record the current start time" and the finalizer is "update the call stack and record the end time", and you want to have the start time be restarted when re-entering a tactic. Nor is it needed for `with_strategy` which needs to update the global conv_oracle so that it plays nicely with `abstract`.) --- engine/proofview.ml | 17 +++++++++++++++++ engine/proofview.mli | 10 ++++++++++ 2 files changed, 27 insertions(+) diff --git a/engine/proofview.ml b/engine/proofview.ml index 2e036be9e3..1d2c7d8729 100644 --- a/engine/proofview.ml +++ b/engine/proofview.ml @@ -297,6 +297,23 @@ let tclIFCATCH a s f = | Nil e -> f e | Cons (x,a') -> plus (s x) (fun e -> (a' e) >>= fun x' -> (s x')) +(** [tclWRAPFINALLY before tac finally] runs [before] before each + entry-point of [tac] and passes the result of [before] to + [finally], which is then run at each exit-point of [tac], + regardless of whether it succeeds or fails. Said another way, if + [tac] succeeds, then it behaves as [before >>= fun v -> tac >>= fun + ret -> finally v <*> tclUNIT ret]; otherwise, if [tac] fails with + [e], it behaves as [before >>= fun v -> finally v <*> tclZERO + e]. *) +let rec tclWRAPFINALLY before tac finally = + let open Logic_monad in + let open Proof in + before >>= fun v -> split tac >>= function + | Nil e -> finally v >>= fun () -> zero e + | Cons (ret,tac') -> plus + (finally v >>= fun () -> return ret) + (fun e -> tclWRAPFINALLY before (tac' e) finally) + (** [tclONCE t] behave like [t] except it has at most one success: [tclONCE t] stops after the first success of [t]. If [t] fails with [e], [tclONCE t] also fails with [e]. *) diff --git a/engine/proofview.mli b/engine/proofview.mli index d0a2b37a69..70513c8166 100644 --- a/engine/proofview.mli +++ b/engine/proofview.mli @@ -208,6 +208,16 @@ val tclORELSE : 'a tactic -> (Exninfo.iexn -> 'a tactic) -> 'a tactic exception can be assumed non critical. *) val tclIFCATCH : 'a tactic -> ('a -> 'b tactic) -> (Exninfo.iexn -> 'b tactic) -> 'b tactic +(** [tclWRAPFINALLY before tac finally] runs [before] before each + entry-point of [tac] and passes the result of [before] to + [finally], which is then run at each exit-point of [tac], + regardless of whether it succeeds or fails. Said another way, if + [tac] succeeds, then it behaves as [before >>= fun v -> tac >>= fun + ret -> finally v <*> tclUNIT ret]; otherwise, if [tac] fails with + [e], it behaves as [before >>= fun v -> finally v <*> tclZERO + e]. *) +val tclWRAPFINALLY : 'a tactic -> 'b tactic -> ('a -> unit tactic) -> 'b tactic + (** [tclONCE t] behave like [t] except it has at most one success: [tclONCE t] stops after the first success of [t]. If [t] fails with [e], [tclONCE t] also fails with [e]. *) -- cgit v1.2.3 From 570dd44feec40ca2be2dd6a4d46ca5378acdce09 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Tue, 28 Apr 2020 15:43:13 -0400 Subject: LtacProf now handles multi-success backtracking Fixes #12196 --- .../12197-ltacprof-multi-success.rst | 8 ++ doc/sphinx/proof-engine/ltac.rst | 18 +++-- plugins/ltac/profile_ltac.ml | 92 ++++++++++------------ test-suite/bugs/closed/bug_12196.v | 46 +++++++++++ test-suite/bugs/closed/bug_6378.v | 9 +++ test-suite/success/ltacprof.v | 17 ++++ 6 files changed, 132 insertions(+), 58 deletions(-) create mode 100644 doc/changelog/05-tactic-language/12197-ltacprof-multi-success.rst create mode 100644 test-suite/bugs/closed/bug_12196.v 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 + `_, `#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. -- cgit v1.2.3 From 206e8adedae1b0c479a2cb598510163f909f1a5f Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Wed, 29 Apr 2020 12:35:58 -0400 Subject: Decrease LtacProf overhead when not profiling Note that this slightly changes the semantics of backtracking across `start ltac profiling`. --- plugins/ltac/profile_ltac.ml | 47 +++++++++++++++++++++++++------------------- 1 file changed, 27 insertions(+), 20 deletions(-) diff --git a/plugins/ltac/profile_ltac.ml b/plugins/ltac/profile_ltac.ml index c89ecb89bd..44cb531e51 100644 --- a/plugins/ltac/profile_ltac.ml +++ b/plugins/ltac/profile_ltac.ml @@ -331,26 +331,33 @@ let exit_tactic ~count_call start_time c = end let do_profile s call_trace ?(count_call=true) 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 ()) + let open Proofview.Notations in + (* We do an early check to [is_profiling] so that we save the + overhead of [Proofview.tclWRAPFINALLY] when profiling is not set + *) + Proofview.tclLIFT (Proofview.NonLogical.make (fun () -> !is_profiling)) >>= function + | false -> tac + | true -> + 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 ************************* *) -- cgit v1.2.3 From 9b937b6f53c5e97faa5c7949e6032837f8708761 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Sat, 2 May 2020 13:25:43 -0400 Subject: Move tclWRAPFINALLY to profile_ltac As per https://github.com/coq/coq/pull/12197#discussion_r418480525 and https://gitter.im/coq/coq?at=5ead5c35347bd616304e83ef --- engine/proofview.ml | 17 ----------------- engine/proofview.mli | 10 ---------- plugins/ltac/profile_ltac.ml | 21 +++++++++++++++++++-- 3 files changed, 19 insertions(+), 29 deletions(-) diff --git a/engine/proofview.ml b/engine/proofview.ml index 1d2c7d8729..2e036be9e3 100644 --- a/engine/proofview.ml +++ b/engine/proofview.ml @@ -297,23 +297,6 @@ let tclIFCATCH a s f = | Nil e -> f e | Cons (x,a') -> plus (s x) (fun e -> (a' e) >>= fun x' -> (s x')) -(** [tclWRAPFINALLY before tac finally] runs [before] before each - entry-point of [tac] and passes the result of [before] to - [finally], which is then run at each exit-point of [tac], - regardless of whether it succeeds or fails. Said another way, if - [tac] succeeds, then it behaves as [before >>= fun v -> tac >>= fun - ret -> finally v <*> tclUNIT ret]; otherwise, if [tac] fails with - [e], it behaves as [before >>= fun v -> finally v <*> tclZERO - e]. *) -let rec tclWRAPFINALLY before tac finally = - let open Logic_monad in - let open Proof in - before >>= fun v -> split tac >>= function - | Nil e -> finally v >>= fun () -> zero e - | Cons (ret,tac') -> plus - (finally v >>= fun () -> return ret) - (fun e -> tclWRAPFINALLY before (tac' e) finally) - (** [tclONCE t] behave like [t] except it has at most one success: [tclONCE t] stops after the first success of [t]. If [t] fails with [e], [tclONCE t] also fails with [e]. *) diff --git a/engine/proofview.mli b/engine/proofview.mli index 70513c8166..d0a2b37a69 100644 --- a/engine/proofview.mli +++ b/engine/proofview.mli @@ -208,16 +208,6 @@ val tclORELSE : 'a tactic -> (Exninfo.iexn -> 'a tactic) -> 'a tactic exception can be assumed non critical. *) val tclIFCATCH : 'a tactic -> ('a -> 'b tactic) -> (Exninfo.iexn -> 'b tactic) -> 'b tactic -(** [tclWRAPFINALLY before tac finally] runs [before] before each - entry-point of [tac] and passes the result of [before] to - [finally], which is then run at each exit-point of [tac], - regardless of whether it succeeds or fails. Said another way, if - [tac] succeeds, then it behaves as [before >>= fun v -> tac >>= fun - ret -> finally v <*> tclUNIT ret]; otherwise, if [tac] fails with - [e], it behaves as [before >>= fun v -> finally v <*> tclZERO - e]. *) -val tclWRAPFINALLY : 'a tactic -> 'b tactic -> ('a -> unit tactic) -> 'b tactic - (** [tclONCE t] behave like [t] except it has at most one success: [tclONCE t] stops after the first success of [t]. If [t] fails with [e], [tclONCE t] also fails with [e]. *) diff --git a/plugins/ltac/profile_ltac.ml b/plugins/ltac/profile_ltac.ml index 44cb531e51..0dbf16a821 100644 --- a/plugins/ltac/profile_ltac.ml +++ b/plugins/ltac/profile_ltac.ml @@ -330,15 +330,32 @@ let exit_tactic ~count_call start_time c = feedback_results parent end +(** [tclWRAPFINALLY before tac finally] runs [before] before each + entry-point of [tac] and passes the result of [before] to + [finally], which is then run at each exit-point of [tac], + regardless of whether it succeeds or fails. Said another way, if + [tac] succeeds, then it behaves as [before >>= fun v -> tac >>= fun + ret -> finally v <*> tclUNIT ret]; otherwise, if [tac] fails with + [e], it behaves as [before >>= fun v -> finally v <*> tclZERO + e]. *) +let rec tclWRAPFINALLY before tac finally = + let open Proofview in + let open Proofview.Notations in + before >>= fun v -> tclCASE tac >>= function + | Fail (e, info) -> finally v >>= fun () -> tclZERO ~info e + | Next (ret, tac') -> tclOR + (finally v >>= fun () -> tclUNIT ret) + (fun e -> tclWRAPFINALLY before (tac' e) finally) + let do_profile s call_trace ?(count_call=true) tac = let open Proofview.Notations in (* We do an early check to [is_profiling] so that we save the - overhead of [Proofview.tclWRAPFINALLY] when profiling is not set + overhead of [tclWRAPFINALLY] when profiling is not set *) Proofview.tclLIFT (Proofview.NonLogical.make (fun () -> !is_profiling)) >>= function | false -> tac | true -> - Proofview.tclWRAPFINALLY + tclWRAPFINALLY (Proofview.tclLIFT (Proofview.NonLogical.make (fun () -> if !is_profiling then match call_trace, Local.(!stack) with -- cgit v1.2.3