Merge PR #9017: Remove SSR profiling

6 files changed, 0 insertions, 193 deletions

diff --git a/plugins/ssr/ssrbwd.ml b/plugins/ssr/ssrbwd.ml
index 1c4508abf4..3e0fbc9a8c 100644
--- a/plugins/ssr/ssrbwd.ml
+++ b/plugins/ssr/ssrbwd.ml
@@ -104,8 +104,6 @@ let mkRAppView ist gl rv gv =
   let nb_view_imps = interp_view_nbimps ist gl rv in
   mkRApp rv (mkRHoles (abs nb_view_imps))
 
-let prof_apply_interp_with = mk_profiler "ssrapplytac.interp_with";;
-
 let refine_interp_apply_view dbl ist gl gv =
   let pair i = List.map (fun x -> i, x) in
   let rv = pf_intern_term ist gl gv in
@@ -113,7 +111,6 @@ let refine_interp_apply_view dbl ist gl gv =
   let interp_with (dbl, hint) =
     let i = if dbl = Ssrview.AdaptorDb.Equivalence then 2 else 1 in
     interp_refine ist gl (mkRApp hint (v :: mkRHoles i)) in
-  let interp_with x = prof_apply_interp_with.profile interp_with x in
   let rec loop = function
   | [] -> (try apply_rconstr ~ist rv gl with _ -> view_error "apply" gv)
   | h :: hs -> (try refine_with (snd (interp_with h)) gl with _ -> loop hs) in
diff --git a/plugins/ssr/ssrcommon.ml b/plugins/ssr/ssrcommon.ml
index 80d421b9fc..fa58a1c39a 100644
--- a/plugins/ssr/ssrcommon.ml
+++ b/plugins/ssr/ssrcommon.ml
@@ -1017,81 +1017,6 @@ let refine_with ?(first_goes_last=false) ?beta ?(with_evars=true) oc gl =
   try applyn ~with_evars ~with_shelve:true ?beta n (EConstr.of_constr oc) gl
   with e when CErrors.noncritical e -> raise dependent_apply_error
 
-(** Profiling *)(* {{{ *************************************************************)
-type profiler = { 
-  profile : 'a 'b. ('a -> 'b) -> 'a -> 'b;
-  reset : unit -> unit;
-  print : unit -> unit }
-let profile_now = ref false
-let something_profiled = ref false
-let profilers = ref []
-let add_profiler f = profilers := f :: !profilers;;
-let _ =
-  Goptions.declare_bool_option
-    { Goptions.optname  = "ssreflect profiling";
-      Goptions.optkey   = ["SsrProfiling"];
-      Goptions.optread  = (fun _ -> !profile_now);
-      Goptions.optdepr  = false;
-      Goptions.optwrite = (fun b -> 
-        Ssrmatching.profile b;
-        profile_now := b;
-        if b then List.iter (fun f -> f.reset ()) !profilers;
-        if not b then List.iter (fun f -> f.print ()) !profilers) }
-let () =
-  let prof_total = 
-    let init = ref 0.0 in { 
-    profile = (fun f x -> assert false);
-    reset = (fun () -> init := Unix.gettimeofday ());
-    print = (fun () -> if !something_profiled then
-        prerr_endline 
-           (Printf.sprintf "!! %-39s %10d %9.4f %9.4f %9.4f"
-           "total" 0 (Unix.gettimeofday() -. !init) 0.0 0.0)) } in
-  let prof_legenda = {
-    profile = (fun f x -> assert false);
-    reset = (fun () -> ());
-    print = (fun () -> if !something_profiled then begin
-        prerr_endline 
-           (Printf.sprintf "!! %39s ---------- --------- --------- ---------" 
-           (String.make 39 '-'));
-        prerr_endline 
-           (Printf.sprintf "!! %-39s %10s %9s %9s %9s" 
-           "function" "#calls" "total" "max" "average") end) } in
-  add_profiler prof_legenda;
-  add_profiler prof_total
-;;
-
-let mk_profiler s =
-  let total, calls, max = ref 0.0, ref 0, ref 0.0 in
-  let reset () = total := 0.0; calls := 0; max := 0.0 in
-  let profile f x =
-    if not !profile_now then f x else
-    let before = Unix.gettimeofday () in
-    try
-      incr calls;
-      let res = f x in
-      let after = Unix.gettimeofday () in
-      let delta = after -. before in
-      total := !total +. delta;
-      if delta > !max then max := delta;
-      res
-    with exc ->
-      let after = Unix.gettimeofday () in
-      let delta = after -. before in
-      total := !total +. delta;
-      if delta > !max then max := delta;
-      raise exc in
-  let print () =
-     if !calls <> 0 then begin
-       something_profiled := true;
-       prerr_endline
-         (Printf.sprintf "!! %-39s %10d %9.4f %9.4f %9.4f" 
-         s !calls !total !max (!total /. (float_of_int !calls))) end in
-  let prof = { profile = profile; reset = reset; print = print } in
-  add_profiler prof;
-  prof
-;;
-(* }}} *)
-
 (* We wipe out all the keywords generated by the grammar rules we defined. *)
 (* The user is supposed to Require Import ssreflect or Require ssreflect   *)
 (* and Import ssreflect.SsrSyntax to obtain these keywords and as a         *)
diff --git a/plugins/ssr/ssrcommon.mli b/plugins/ssr/ssrcommon.mli
index cf4e4b354e..e92489e568 100644
--- a/plugins/ssr/ssrcommon.mli
+++ b/plugins/ssr/ssrcommon.mli
@@ -378,13 +378,6 @@ val pf_interp_gen_aux :
 val is_name_in_ipats :
            Id.t -> ssripats -> bool
 
-type profiler = { 
-  profile : 'a 'b. ('a -> 'b) -> 'a -> 'b;
-  reset : unit -> unit;
-  print : unit -> unit }
-
-val mk_profiler : string -> profiler
-
 (** Basic tactics *)
 
 val introid : ?orig:Name.t ref -> Id.t -> v82tac
diff --git a/plugins/ssr/ssrequality.ml b/plugins/ssr/ssrequality.ml
index 2a69e3f23a..22475fef34 100644
--- a/plugins/ssr/ssrequality.ml
+++ b/plugins/ssr/ssrequality.ml
@@ -425,11 +425,6 @@ let rwcltac cl rdx dir sr gl =
   in
   tclTHEN cvtac' rwtac gl
 
-let prof_rwcltac = mk_profiler "rwrxtac.rwcltac";;
-let rwcltac cl rdx dir sr gl =
-  prof_rwcltac.profile (rwcltac cl rdx dir sr) gl
-;;
-
 
 [@@@ocaml.warning "-3"]
 let lz_coq_prod =
@@ -455,8 +450,6 @@ let ssr_is_setoid env =
     Rewrite.is_applied_rewrite_relation env 
       sigma [] (EConstr.mkApp (r, args)) <> None
 
-let prof_rwxrtac_find_rule = mk_profiler "rwrxtac.find_rule";;
-
 let closed0_check cl p gl =
   if closed0 cl then
     errorstrm Pp.(str"No occurrence of redex "++ pr_constr_env (pf_env gl) (project gl) p)
@@ -556,7 +549,6 @@ let rwrxtac occ rdx_pat dir rule gl =
           d, (ise, Evd.evar_universe_context ise, Reductionops.nf_evar ise r)
         with _ -> rwtac rs in
      rwtac rules in
-  let find_rule rdx = prof_rwxrtac_find_rule.profile find_rule rdx in
   let sigma0, env0, concl0 = project gl, pf_env gl, pf_concl gl in
   let find_R, conclude = match rdx_pat with
   | Some (_, (In_T _ | In_X_In_T _)) | None ->
@@ -582,11 +574,6 @@ let rwrxtac occ rdx_pat dir rule gl =
   rwcltac (EConstr.of_constr concl) (EConstr.of_constr rdx) d r gl
 ;;
 
-let prof_rwxrtac = mk_profiler "rwrxtac";;
-let rwrxtac occ rdx_pat dir rule gl =
-  prof_rwxrtac.profile (rwrxtac occ rdx_pat dir rule) gl
-;;
-
 let ssrinstancesofrule ist dir arg gl =
   let sigma0, env0, concl0 = project gl, pf_env gl, pf_concl gl in
   let rule = interp_term ist gl arg in
diff --git a/plugins/ssrmatching/ssrmatching.ml b/plugins/ssrmatching/ssrmatching.ml
index 142d1ac790..8cb0a8b463 100644
--- a/plugins/ssrmatching/ssrmatching.ml
+++ b/plugins/ssrmatching/ssrmatching.ml
@@ -174,82 +174,6 @@ let nf_evar sigma c =
 
 (* }}} *)
 
-(** Profiling *)(* {{{ *************************************************************)
-type profiler = { 
-  profile : 'a 'b. ('a -> 'b) -> 'a -> 'b;
-  reset : unit -> unit;
-  print : unit -> unit }
-let profile_now = ref false
-let something_profiled = ref false
-let profilers = ref []
-let add_profiler f = profilers := f :: !profilers;;
-let profile b =
-  profile_now := b;
-  if b then List.iter (fun f -> f.reset ()) !profilers;
-  if not b then List.iter (fun f -> f.print ()) !profilers
-;;
-let _ =
-  Goptions.declare_bool_option
-    { Goptions.optname  = "ssrmatching profiling";
-      Goptions.optkey   = ["SsrMatchingProfiling"];
-      Goptions.optread  = (fun _ -> !profile_now);
-      Goptions.optdepr  = false;
-      Goptions.optwrite = profile }
-let () =
-  let prof_total = 
-    let init = ref 0.0 in { 
-    profile = (fun f x -> assert false);
-    reset = (fun () -> init := Unix.gettimeofday ());
-    print = (fun () -> if !something_profiled then
-        prerr_endline 
-           (Printf.sprintf "!! %-39s %10d %9.4f %9.4f %9.4f"
-           "total" 0 (Unix.gettimeofday() -. !init) 0.0 0.0)) } in
-  let prof_legenda = {
-    profile = (fun f x -> assert false);
-    reset = (fun () -> ());
-    print = (fun () -> if !something_profiled then begin
-        prerr_endline 
-           (Printf.sprintf "!! %39s ---------- --------- --------- ---------" 
-           (String.make 39 '-'));
-        prerr_endline 
-           (Printf.sprintf "!! %-39s %10s %9s %9s %9s" 
-           "function" "#calls" "total" "max" "average") end) } in
-  add_profiler prof_legenda;
-  add_profiler prof_total
-;;
-
-let mk_profiler s =
-  let total, calls, max = ref 0.0, ref 0, ref 0.0 in
-  let reset () = total := 0.0; calls := 0; max := 0.0 in
-  let profile f x =
-    if not !profile_now then f x else
-    let before = Unix.gettimeofday () in
-    try
-      incr calls;
-      let res = f x in
-      let after = Unix.gettimeofday () in
-      let delta = after -. before in
-      total := !total +. delta;
-      if delta > !max then max := delta;
-      res
-    with exc ->
-      let after = Unix.gettimeofday () in
-      let delta = after -. before in
-      total := !total +. delta;
-      if delta > !max then max := delta;
-      raise exc in
-  let print () =
-     if !calls <> 0 then begin
-       something_profiled := true;
-       prerr_endline
-         (Printf.sprintf "!! %-39s %10d %9.4f %9.4f %9.4f" 
-         s !calls !total !max (!total /. (float_of_int !calls))) end in
-  let prof = { profile = profile; reset = reset; print = print } in
-  add_profiler prof;
-  prof
-;;
-(* }}} *)
-
 exception NoProgress
 
 (** Unification procedures.                                *)
@@ -286,11 +210,6 @@ let unif_EQ_args env sigma pa a =
   let rec loop i = (i = n) || unif_EQ env sigma pa.(i) a.(i) && loop (i + 1) in
   loop 0
 
-let prof_unif_eq_args = mk_profiler "unif_EQ_args";;
-let unif_EQ_args env sigma pa a =
-  prof_unif_eq_args.profile (unif_EQ_args env sigma pa) a 
-;;
-
 let unif_HO env ise p c =
   try Evarconv.the_conv_x env p c ise
   with Evarconv.UnableToUnify(ise, err) ->
@@ -650,11 +569,6 @@ let match_upats_FO upats env sigma0 ise orig_c =
   iter_constr_LR loop f; Array.iter loop a in
   try loop orig_c with Invalid_argument _ -> CErrors.anomaly (str"IN FO.")
 
-let prof_FO = mk_profiler "match_upats_FO";;
-let match_upats_FO upats env sigma0 ise c =
-  prof_FO.profile (match_upats_FO upats env sigma0) ise c
-;;
-
 
 let match_upats_HO ~on_instance upats env sigma0 ise c =
  let dont_impact_evars = dont_impact_evars_in c in
@@ -706,11 +620,6 @@ let match_upats_HO ~on_instance upats env sigma0 ise c =
  if !it_did_match then raise NoProgress;
  !failed_because_of_TC
 
-let prof_HO = mk_profiler "match_upats_HO";;
-let match_upats_HO ~on_instance upats env sigma0 ise c =
-  prof_HO.profile (match_upats_HO ~on_instance upats env sigma0) ise c
-;;
-
 
 let fixed_upat evd = function
 | {up_k = KpatFlex | KpatEvar _ | KpatProj _} -> false 
diff --git a/plugins/ssrmatching/ssrmatching.mli b/plugins/ssrmatching/ssrmatching.mli
index b3ddb52e85..63b7e1783e 100644
--- a/plugins/ssrmatching/ssrmatching.mli
+++ b/plugins/ssrmatching/ssrmatching.mli
@@ -221,10 +221,6 @@ val pf_unsafe_merge_uc : UState.t -> goal Evd.sigma -> goal Evd.sigma
 (* One can also "Set SsrMatchingDebug" from a .v *)
 val debug : bool -> unit
 
-(* One should delimit a snippet with "Set SsrMatchingProfiling" and
- * "Unset SsrMatchingProfiling" to get timings *)
-val profile : bool -> unit
-
 val ssrinstancesof : cpattern -> Tacmach.tactic
 
 (** Functions used for grammar extensions. Do not use. *)