Remove SSR profiling

Deletes the SsrProfiling and SsrMatchingProfiling options

4 files changed, 0 insertions, 98 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 ddfd4c101f..648bb00d5c 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