From d0f89f8c59cda2e7e74fec693e511e910fbc0434 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Tue, 5 Dec 2017 12:34:36 +0100 Subject: [lib] Rename Profile to CProfile New module introduced in OCaml 4.05 I think, can create problems when linking with the OCaml toplevel for `Drop`. --- checker/inductive.ml | 4 +- dev/doc/debugging.md | 4 +- engine/uState.ml | 4 +- engine/universes.ml | 4 +- kernel/cooking.ml | 4 +- kernel/inductive.ml | 4 +- kernel/reduction.ml | 16 +- kernel/typeops.ml | 4 +- kernel/uGraph.ml | 16 +- kernel/vars.ml | 12 +- lib/cProfile.ml | 714 ++++++++++++++++++++++++++++++++++++++++++++++ lib/cProfile.mli | 119 ++++++++ lib/lib.mllib | 2 +- lib/profile.ml | 714 ---------------------------------------------- lib/profile.mli | 119 -------- plugins/ltac/rewrite.ml | 8 +- pretyping/evarconv.ml | 4 +- pretyping/reductionops.ml | 8 +- pretyping/retyping.ml | 4 +- pretyping/tacred.ml | 4 +- pretyping/typeclasses.ml | 4 +- pretyping/unification.ml | 4 +- proofs/refiner.ml | 4 +- tactics/auto.ml | 4 +- tactics/eauto.ml | 4 +- tactics/tactics.ml | 8 +- toplevel/coqtop.ml | 4 +- 27 files changed, 900 insertions(+), 900 deletions(-) create mode 100644 lib/cProfile.ml create mode 100644 lib/cProfile.mli delete mode 100644 lib/profile.ml delete mode 100644 lib/profile.mli diff --git a/checker/inductive.ml b/checker/inductive.ml index 1271a02b0..22353ec16 100644 --- a/checker/inductive.ml +++ b/checker/inductive.ml @@ -1070,8 +1070,8 @@ let check_fix env ((nvect,_),(names,_,bodies as _recdef) as fix) = done (* -let cfkey = Profile.declare_profile "check_fix";; -let check_fix env fix = Profile.profile3 cfkey check_fix env fix;; +let cfkey = CProfile.declare_profile "check_fix";; +let check_fix env fix = CProfile.profile3 cfkey check_fix env fix;; *) (************************************************************************) diff --git a/dev/doc/debugging.md b/dev/doc/debugging.md index 7d3d811cc..fa145d498 100644 --- a/dev/doc/debugging.md +++ b/dev/doc/debugging.md @@ -73,8 +73,8 @@ Per function profiling To profile function foo in file bar.ml, add the following lines, just after the definition of the function: - let fookey = Profile.declare_profile "foo";; - let foo a b c = Profile.profile3 fookey foo a b c;; + let fookey = CProfile.declare_profile "foo";; + let foo a b c = CProfile.profile3 fookey foo a b c;; where foo is assumed to have three arguments (adapt using Profile.profile1, Profile. profile2, etc). diff --git a/engine/uState.ml b/engine/uState.ml index c28e78f7d..9510371be 100644 --- a/engine/uState.ml +++ b/engine/uState.ml @@ -236,8 +236,8 @@ let add_constraints ctx cstrs = uctx_univ_variables = vars; uctx_universes = UGraph.merge_constraints local' ctx.uctx_universes } -(* let addconstrkey = Profile.declare_profile "add_constraints_context";; *) -(* let add_constraints_context = Profile.profile2 addconstrkey add_constraints_context;; *) +(* let addconstrkey = CProfile.declare_profile "add_constraints_context";; *) +(* let add_constraints_context = CProfile.profile2 addconstrkey add_constraints_context;; *) let add_universe_constraints ctx cstrs = let univs, local = ctx.uctx_local in diff --git a/engine/universes.ml b/engine/universes.ml index 0250295fd..30490ec56 100644 --- a/engine/universes.ml +++ b/engine/universes.ml @@ -946,8 +946,8 @@ let normalize_context_set ctx us algs = let us = normalize_opt_subst us in (us, algs), (ctx', Constraint.union noneqs eqs) -(* let normalize_conkey = Profile.declare_profile "normalize_context_set" *) -(* let normalize_context_set a b c = Profile.profile3 normalize_conkey normalize_context_set a b c *) +(* let normalize_conkey = CProfile.declare_profile "normalize_context_set" *) +(* let normalize_context_set a b c = CProfile.profile3 normalize_conkey normalize_context_set a b c *) let is_trivial_leq (l,d,r) = Univ.Level.is_prop l && (d == Univ.Le || (d == Univ.Lt && Univ.Level.is_set r)) diff --git a/kernel/cooking.ml b/kernel/cooking.ml index 2579ac045..7b921d35b 100644 --- a/kernel/cooking.ml +++ b/kernel/cooking.ml @@ -250,7 +250,7 @@ let cook_constant ~hcons env { from = cb; info } = cook_context = Some const_hyps; } -(* let cook_constant_key = Profile.declare_profile "cook_constant" *) -(* let cook_constant = Profile.profile2 cook_constant_key cook_constant *) +(* let cook_constant_key = CProfile.declare_profile "cook_constant" *) +(* let cook_constant = CProfile.profile2 cook_constant_key cook_constant *) let expmod_constr modlist c = expmod_constr (RefTable.create 13) modlist c diff --git a/kernel/inductive.ml b/kernel/inductive.ml index 62aa9a2d7..2a629f00a 100644 --- a/kernel/inductive.ml +++ b/kernel/inductive.ml @@ -1098,8 +1098,8 @@ let check_fix env ((nvect,_),(names,_,bodies as recdef) as fix) = () (* -let cfkey = Profile.declare_profile "check_fix";; -let check_fix env fix = Profile.profile3 cfkey check_fix env fix;; +let cfkey = CProfile.declare_profile "check_fix";; +let check_fix env fix = CProfile.profile3 cfkey check_fix env fix;; *) (************************************************************************) diff --git a/kernel/reduction.ml b/kernel/reduction.ml index 41d6c05eb..ca67c5f13 100644 --- a/kernel/reduction.ml +++ b/kernel/reduction.ml @@ -833,8 +833,8 @@ let gen_conv cv_pb l2r reds env evars univs t1 t2 = let gen_conv cv_pb ?(l2r=false) ?(reds=full_transparent_state) env ?(evars=(fun _->None), universes env) = let evars, univs = evars in if Flags.profile then - let fconv_universes_key = Profile.declare_profile "trans_fconv_universes" in - Profile.profile8 fconv_universes_key gen_conv cv_pb l2r reds env evars univs + let fconv_universes_key = CProfile.declare_profile "trans_fconv_universes" in + CProfile.profile8 fconv_universes_key gen_conv cv_pb l2r reds env evars univs else gen_conv cv_pb l2r reds env evars univs let conv = gen_conv CONV @@ -860,8 +860,8 @@ let infer_conv_universes cv_pb l2r evars reds env univs t1 t2 = (* Profiling *) let infer_conv_universes = if Flags.profile then - let infer_conv_universes_key = Profile.declare_profile "infer_conv_universes" in - Profile.profile8 infer_conv_universes_key infer_conv_universes + let infer_conv_universes_key = CProfile.declare_profile "infer_conv_universes" in + CProfile.profile8 infer_conv_universes_key infer_conv_universes else infer_conv_universes let infer_conv ?(l2r=false) ?(evars=fun _ -> None) ?(ts=full_transparent_state) @@ -895,13 +895,13 @@ let default_conv cv_pb ?(l2r=false) env t1 t2 = let default_conv_leq = default_conv CUMUL (* -let convleqkey = Profile.declare_profile "Kernel_reduction.conv_leq";; +let convleqkey = CProfile.declare_profile "Kernel_reduction.conv_leq";; let conv_leq env t1 t2 = - Profile.profile4 convleqkey conv_leq env t1 t2;; + CProfile.profile4 convleqkey conv_leq env t1 t2;; -let convkey = Profile.declare_profile "Kernel_reduction.conv";; +let convkey = CProfile.declare_profile "Kernel_reduction.conv";; let conv env t1 t2 = - Profile.profile4 convleqkey conv env t1 t2;; + CProfile.profile4 convleqkey conv env t1 t2;; *) (* Application with on-the-fly reduction *) diff --git a/kernel/typeops.ml b/kernel/typeops.ml index 4ccef5c38..4a935f581 100644 --- a/kernel/typeops.ml +++ b/kernel/typeops.ml @@ -435,8 +435,8 @@ let infer env constr = let infer = if Flags.profile then - let infer_key = Profile.declare_profile "Fast_infer" in - Profile.profile2 infer_key (fun b c -> infer b c) + let infer_key = CProfile.declare_profile "Fast_infer" in + CProfile.profile2 infer_key (fun b c -> infer b c) else (fun b c -> infer b c) let assumption_of_judgment env {uj_val=c; uj_type=t} = diff --git a/kernel/uGraph.ml b/kernel/uGraph.ml index 00c0ea70d..f1e8d1031 100644 --- a/kernel/uGraph.ml +++ b/kernel/uGraph.ml @@ -890,24 +890,24 @@ let dump_universes output g = let merge_constraints = if Flags.profile then - let key = Profile.declare_profile "merge_constraints" in - Profile.profile2 key merge_constraints + let key = CProfile.declare_profile "merge_constraints" in + CProfile.profile2 key merge_constraints else merge_constraints let check_constraints = if Flags.profile then - let key = Profile.declare_profile "check_constraints" in - Profile.profile2 key check_constraints + let key = CProfile.declare_profile "check_constraints" in + CProfile.profile2 key check_constraints else check_constraints let check_eq = if Flags.profile then - let check_eq_key = Profile.declare_profile "check_eq" in - Profile.profile3 check_eq_key check_eq + let check_eq_key = CProfile.declare_profile "check_eq" in + CProfile.profile3 check_eq_key check_eq else check_eq let check_leq = if Flags.profile then - let check_leq_key = Profile.declare_profile "check_leq" in - Profile.profile3 check_leq_key check_leq + let check_leq_key = CProfile.declare_profile "check_leq" in + CProfile.profile3 check_leq_key check_leq else check_leq diff --git a/kernel/vars.ml b/kernel/vars.ml index f52d734ef..eae917b5a 100644 --- a/kernel/vars.ml +++ b/kernel/vars.ml @@ -133,8 +133,8 @@ let substn_many lamv n c = substrec n c (* -let substkey = Profile.declare_profile "substn_many";; -let substn_many lamv n c = Profile.profile3 substkey substn_many lamv n c;; +let substkey = CProfile.declare_profile "substn_many";; +let substn_many lamv n c = CProfile.profile3 substkey substn_many lamv n c;; *) let make_subst = function @@ -274,8 +274,8 @@ let subst_univs_constr subst c = let subst_univs_constr = if Flags.profile then - let subst_univs_constr_key = Profile.declare_profile "subst_univs_constr" in - Profile.profile2 subst_univs_constr_key subst_univs_constr + let subst_univs_constr_key = CProfile.declare_profile "subst_univs_constr" in + CProfile.profile2 subst_univs_constr_key subst_univs_constr else subst_univs_constr let subst_univs_level_constr subst c = @@ -347,8 +347,8 @@ let subst_instance_constr subst c = in aux c -(* let substkey = Profile.declare_profile "subst_instance_constr";; *) -(* let subst_instance_constr inst c = Profile.profile2 substkey subst_instance_constr inst c;; *) +(* let substkey = CProfile.declare_profile "subst_instance_constr";; *) +(* let subst_instance_constr inst c = CProfile.profile2 substkey subst_instance_constr inst c;; *) let subst_instance_context s ctx = if Univ.Instance.is_empty s then ctx diff --git a/lib/cProfile.ml b/lib/cProfile.ml new file mode 100644 index 000000000..0bc226a45 --- /dev/null +++ b/lib/cProfile.ml @@ -0,0 +1,714 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* [] || Flags.profile then begin + let outside = create_record () in + stack := [outside]; + last_alloc := get_alloc (); + init_alloc := !last_alloc; + init_time := get_time (); + outside.tottime <- - !init_time; + outside.owntime <- - !init_time + end + +let ajoute n o = + o.owntime <- o.owntime + n.owntime; + o.tottime <- o.tottime + n.tottime; + ajoute_ownalloc o n.ownalloc; + ajoute_totalloc o n.totalloc; + o.owncount <- o.owncount + n.owncount; + o.intcount <- o.intcount + n.intcount; + o.immcount <- o.immcount + n.immcount + +let ajoute_to_list ((name,n) as e) l = + try ajoute n (List.assoc name l); l + with Not_found -> e::l + +let magic = 1249 + +let merge_profile filename (curr_table, curr_outside, curr_total as new_data) = + let (old_table, old_outside, old_total) = + try + let c = open_in filename in + if input_binary_int c <> magic + then Printf.printf "Incompatible recording file: %s\n" filename; + let old_data = input_value c in + close_in c; + old_data + with Sys_error msg -> + (Printf.printf "Unable to open %s: %s\n" filename msg; + new_data) in + let updated_data = + let updated_table = List.fold_right ajoute_to_list curr_table old_table in + ajoute curr_outside old_outside; + ajoute curr_total old_total; + (updated_table, old_outside, old_total) in + begin + (try + let c = + open_out_gen + [Open_creat;Open_wronly;Open_trunc;Open_binary] 0o644 filename in + output_binary_int c magic; + output_value c updated_data; + close_out c + with Sys_error _ -> Printf.printf "Unable to create recording file"); + updated_data + end + +(************************************************) +(* Compute a rough estimation of time overheads *) + +(* Time and space are not measured in the same way *) + +(* Byte allocation is an exact number and for long runs, the total + number of allocated bytes may exceed the maximum integer capacity + (2^31 on 32-bits architectures); therefore, allocation is measured + by small steps, total allocations are computed by adding elementary + measures and carries are controlled from step to step *) + +(* Unix measure of time is approximate and short delays are often + unperceivable; therefore, total times are measured in one (big) + step to avoid rounding errors and to get the best possible + approximation. + Note: Sys.time is the same as: + Unix.(let x = times () in x.tms_utime +. x.tms_stime) + *) + +(* +---------- start profile for f1 +overheadA| ... + ---------- [1w1] 1st call to get_time for f1 + overheadB| ... + ---------- start f1 + real 1 | ... + ---------- start profile for 1st call to f2 inside f1 + overheadA| ... + ---------- [2w1] 1st call to get_time for 1st f2 + overheadB| ... + ---------- start 1st f2 + real 2 | ... + ---------- end 1st f2 + overheadC| ... + ---------- [2w1] 2nd call to get_time for 1st f2 + overheadD| ... + ---------- end profile for 1st f2 + real 1 | ... + ---------- start profile for 2nd call to f2 inside f1 + overheadA| ... + ---------- [2'w1] 1st call to get_time for 2nd f2 + overheadB| ... + ---------- start 2nd f2 + real 2' | ... + ---------- end 2nd f2 + overheadC| ... + ---------- [2'w2] 2nd call to get_time for 2nd f2 + overheadD| ... + ---------- end profile for f2 + real 1 | ... + ---------- end f1 + overheadC| ... +---------- [1w1'] 2nd call to get_time for f1 +overheadD| ... +---------- end profile for f1 + +When profiling f2, overheadB + overheadC should be subtracted from measure +and overheadA + overheadB + overheadC + overheadD should be subtracted from +the amount for f1 + +Then the relevant overheads are : + + "overheadB + overheadC" to be subtracted to the measure of f as many time as f is called and + + "overheadA + overheadB + overheadC + overheadD" to be subtracted to + the measure of f as many time as f calls a profiled function (itself + included) +*) + +let dummy_last_alloc = ref 0.0 +let dummy_spent_alloc () = + let now = get_alloc () in + let before = !last_alloc in + last_alloc := now; + now -. before +let dummy_f x = x +let dummy_stack = ref [create_record ()] +let dummy_ov = 0 + +let loops = 10000 + +let time_overhead_A_D () = + let e = create_record () in + let before = get_time () in + for _i = 1 to loops do + (* This is a copy of profile1 for overhead estimation *) + let dw = dummy_spent_alloc () in + match !dummy_stack with [] -> assert false | p::_ -> + ajoute_ownalloc p dw; + ajoute_totalloc p dw; + e.owncount <- e.owncount + 1; + if not (p==e) then stack := e::!stack; + let totalloc0 = e.totalloc in + let intcount0 = e.intcount in + let dt = get_time () - 1 in + e.tottime <- dt + dummy_ov; e.owntime <- e.owntime + e.tottime; + ajoute_ownalloc p dw; + ajoute_totalloc p dw; + p.owntime <- p.owntime - e.tottime; + ajoute_totalloc p (e.totalloc-.totalloc0); + p.intcount <- p.intcount + e.intcount - intcount0 + 1; + p.immcount <- p.immcount + 1; + if not (p==e) then + (match !dummy_stack with [] -> assert false | _::s -> stack := s); + dummy_last_alloc := get_alloc () + done; + let after = get_time () in + let beforeloop = get_time () in + for _i = 1 to loops do () done; + let afterloop = get_time () in + float_of_int ((after - before) - (afterloop - beforeloop)) + /. float_of_int loops + +let time_overhead_B_C () = + let dummy_x = 0 in + let before = get_time () in + for _i = 1 to loops do + try + dummy_last_alloc := get_alloc (); + let _r = dummy_f dummy_x in + let _dw = dummy_spent_alloc () in + let _dt = get_time () in + () + with e when CErrors.noncritical e -> assert false + done; + let after = get_time () in + let beforeloop = get_time () in + for _i = 1 to loops do () done; + let afterloop = get_time () in + float_of_int ((after - before) - (afterloop - beforeloop)) + /. float_of_int loops + +let compute_alloc lo = lo /. (float_of_int word_length) + +(************************************************) +(* End a profiling session and print the result *) + +let format_profile (table, outside, total) = + print_newline (); + Printf.printf + "%-23s %9s %9s %10s %10s %10s\n" + "Function name" "Own time" "Tot. time" "Own alloc" "Tot. alloc" "Calls "; + let l = List.sort (fun (_,{tottime=p}) (_,{tottime=p'}) -> p' - p) table in + List.iter (fun (name,e) -> + Printf.printf + "%-23s %9.2f %9.2f %10.0f %10.0f %6d %6d\n" + name + (float_of_time e.owntime) (float_of_time e.tottime) + (compute_alloc e.ownalloc) + (compute_alloc e.totalloc) + e.owncount e.intcount) + l; + Printf.printf "%-23s %9.2f %9.2f %10.0f %10.0f %6d\n" + "others" + (float_of_time outside.owntime) (float_of_time outside.tottime) + (compute_alloc outside.ownalloc) + (compute_alloc outside.totalloc) + outside.intcount; + (* Here, own contains overhead time/alloc *) + Printf.printf "%-23s %9.2f %9.2f %10.0f %10.0f\n" + "Est. overhead/total" + (float_of_time total.owntime) (float_of_time total.tottime) + (compute_alloc total.ownalloc) + (compute_alloc total.totalloc); + Printf.printf + "Time in seconds and allocation in words (1 word = %d bytes)\n" + word_length + +let recording_file = ref "" +let set_recording s = recording_file := s + +let adjust_time ov_bc ov_ad e = + let bc_imm = float_of_int e.owncount *. ov_bc in + let ad_imm = float_of_int e.immcount *. ov_ad in + let abcd_all = float_of_int e.intcount *. (ov_ad +. ov_bc) in + {e with + tottime = e.tottime - int_of_float (abcd_all +. bc_imm); + owntime = e.owntime - int_of_float (ad_imm +. bc_imm) } + +let close_profile print = + if !prof_table <> [] then begin + let dw = spent_alloc () in + let t = get_time () in + match !stack with + | [outside] -> + outside.tottime <- outside.tottime + t; + outside.owntime <- outside.owntime + t; + ajoute_ownalloc outside dw; + ajoute_totalloc outside dw; + let ov_bc = time_overhead_B_C () (* B+C overhead *) in + let ov_ad = time_overhead_A_D () (* A+D overhead *) in + let adjust (n,e) = (n, adjust_time ov_bc ov_ad e) in + let adjtable = List.map adjust !prof_table in + let adjoutside = adjust_time ov_bc ov_ad outside in + let totalloc = !last_alloc -. !init_alloc in + let total = create_record () in + total.tottime <- outside.tottime; + total.totalloc <- totalloc; + (* We compute estimations of overhead, put into "own" fields *) + total.owntime <- outside.tottime - adjoutside.tottime; + total.ownalloc <- totalloc -. outside.totalloc; + let current_data = (adjtable, adjoutside, total) in + let updated_data = + match !recording_file with + | "" -> current_data + | name -> merge_profile !recording_file current_data + in + if print then format_profile updated_data; + init_profile () + | _ -> failwith "Inconsistency" + end + +let print_profile () = close_profile true + +let declare_profile name = + if name = "___outside___" || name = "___total___" then + failwith ("Error: "^name^" is a reserved keyword"); + let e = create_record () in + prof_table := (name,e)::!prof_table; + e + +(******************************) +(* Entry points for profiling *) +let profile1 e f a = + let dw = spent_alloc () in + match !stack with [] -> assert false | p::_ -> + (* We add spent alloc since last measure to current caller own/total alloc *) + ajoute_ownalloc p dw; + ajoute_totalloc p dw; + e.owncount <- e.owncount + 1; + if not (p==e) then stack := e::!stack; + let totalloc0 = e.totalloc in + let intcount0 = e.intcount in + let t = get_time () in + try + last_alloc := get_alloc (); + let r = f a in + let dw = spent_alloc () in + let dt = get_time () - t in + e.tottime <- e.tottime + dt; e.owntime <- e.owntime + dt; + ajoute_ownalloc e dw; + ajoute_totalloc e dw; + p.owntime <- p.owntime - dt; + ajoute_totalloc p (e.totalloc -. totalloc0); + p.intcount <- p.intcount + e.intcount - intcount0 + 1; + p.immcount <- p.immcount + 1; + if not (p==e) then + (match !stack with [] -> assert false | _::s -> stack := s); + last_alloc := get_alloc (); + r + with reraise -> + let dw = spent_alloc () in + let dt = get_time () - t in + e.tottime <- e.tottime + dt; e.owntime <- e.owntime + dt; + ajoute_ownalloc e dw; + ajoute_totalloc e dw; + p.owntime <- p.owntime - dt; + ajoute_totalloc p (e.totalloc -. totalloc0); + p.intcount <- p.intcount + e.intcount - intcount0 + 1; + p.immcount <- p.immcount + 1; + if not (p==e) then + (match !stack with [] -> assert false | _::s -> stack := s); + last_alloc := get_alloc (); + raise reraise + +let profile2 e f a b = + let dw = spent_alloc () in + match !stack with [] -> assert false | p::_ -> + (* We add spent alloc since last measure to current caller own/total alloc *) + ajoute_ownalloc p dw; + ajoute_totalloc p dw; + e.owncount <- e.owncount + 1; + if not (p==e) then stack := e::!stack; + let totalloc0 = e.totalloc in + let intcount0 = e.intcount in + let t = get_time () in + try + last_alloc := get_alloc (); + let r = f a b in + let dw = spent_alloc () in + let dt = get_time () - t in + e.tottime <- e.tottime + dt; e.owntime <- e.owntime + dt; + ajoute_ownalloc e dw; + ajoute_totalloc e dw; + p.owntime <- p.owntime - dt; + ajoute_totalloc p (e.totalloc -. totalloc0); + p.intcount <- p.intcount + e.intcount - intcount0 + 1; + p.immcount <- p.immcount + 1; + if not (p==e) then + (match !stack with [] -> assert false | _::s -> stack := s); + last_alloc := get_alloc (); + r + with reraise -> + let dw = spent_alloc () in + let dt = get_time () - t in + e.tottime <- e.tottime + dt; e.owntime <- e.owntime + dt; + ajoute_ownalloc e dw; + ajoute_totalloc e dw; + p.owntime <- p.owntime - dt; + ajoute_totalloc p (e.totalloc -. totalloc0); + p.intcount <- p.intcount + e.intcount - intcount0 + 1; + p.immcount <- p.immcount + 1; + if not (p==e) then + (match !stack with [] -> assert false | _::s -> stack := s); + last_alloc := get_alloc (); + raise reraise + +let profile3 e f a b c = + let dw = spent_alloc () in + match !stack with [] -> assert false | p::_ -> + (* We add spent alloc since last measure to current caller own/total alloc *) + ajoute_ownalloc p dw; + ajoute_totalloc p dw; + e.owncount <- e.owncount + 1; + if not (p==e) then stack := e::!stack; + let totalloc0 = e.totalloc in + let intcount0 = e.intcount in + let t = get_time () in + try + last_alloc := get_alloc (); + let r = f a b c in + let dw = spent_alloc () in + let dt = get_time () - t in + e.tottime <- e.tottime + dt; e.owntime <- e.owntime + dt; + ajoute_ownalloc e dw; + ajoute_totalloc e dw; + p.owntime <- p.owntime - dt; + ajoute_totalloc p (e.totalloc -. totalloc0); + p.intcount <- p.intcount + e.intcount - intcount0 + 1; + p.immcount <- p.immcount + 1; + if not (p==e) then + (match !stack with [] -> assert false | _::s -> stack := s); + last_alloc := get_alloc (); + r + with reraise -> + let dw = spent_alloc () in + let dt = get_time () - t in + e.tottime <- e.tottime + dt; e.owntime <- e.owntime + dt; + ajoute_ownalloc e dw; + ajoute_totalloc e dw; + p.owntime <- p.owntime - dt; + ajoute_totalloc p (e.totalloc -. totalloc0); + p.intcount <- p.intcount + e.intcount - intcount0 + 1; + p.immcount <- p.immcount + 1; + if not (p==e) then + (match !stack with [] -> assert false | _::s -> stack := s); + last_alloc := get_alloc (); + raise reraise + +let profile4 e f a b c d = + let dw = spent_alloc () in + match !stack with [] -> assert false | p::_ -> + (* We add spent alloc since last measure to current caller own/total alloc *) + ajoute_ownalloc p dw; + ajoute_totalloc p dw; + e.owncount <- e.owncount + 1; + if not (p==e) then stack := e::!stack; + let totalloc0 = e.totalloc in + let intcount0 = e.intcount in + let t = get_time () in + try + last_alloc := get_alloc (); + let r = f a b c d in + let dw = spent_alloc () in + let dt = get_time () - t in + e.tottime <- e.tottime + dt; e.owntime <- e.owntime + dt; + ajoute_ownalloc e dw; + ajoute_totalloc e dw; + p.owntime <- p.owntime - dt; + ajoute_totalloc p (e.totalloc -. totalloc0); + p.intcount <- p.intcount + e.intcount - intcount0 + 1; + p.immcount <- p.immcount + 1; + if not (p==e) then + (match !stack with [] -> assert false | _::s -> stack := s); + last_alloc := get_alloc (); + r + with reraise -> + let dw = spent_alloc () in + let dt = get_time () - t in + e.tottime <- e.tottime + dt; e.owntime <- e.owntime + dt; + ajoute_ownalloc e dw; + ajoute_totalloc e dw; + p.owntime <- p.owntime - dt; + ajoute_totalloc p (e.totalloc -. totalloc0); + p.intcount <- p.intcount + e.intcount - intcount0 + 1; + p.immcount <- p.immcount + 1; + if not (p==e) then + (match !stack with [] -> assert false | _::s -> stack := s); + last_alloc := get_alloc (); + raise reraise + +let profile5 e f a b c d g = + let dw = spent_alloc () in + match !stack with [] -> assert false | p::_ -> + (* We add spent alloc since last measure to current caller own/total alloc *) + ajoute_ownalloc p dw; + ajoute_totalloc p dw; + e.owncount <- e.owncount + 1; + if not (p==e) then stack := e::!stack; + let totalloc0 = e.totalloc in + let intcount0 = e.intcount in + let t = get_time () in + try + last_alloc := get_alloc (); + let r = f a b c d g in + let dw = spent_alloc () in + let dt = get_time () - t in + e.tottime <- e.tottime + dt; e.owntime <- e.owntime + dt; + ajoute_ownalloc e dw; + ajoute_totalloc e dw; + p.owntime <- p.owntime - dt; + ajoute_totalloc p (e.totalloc -. totalloc0); + p.intcount <- p.intcount + e.intcount - intcount0 + 1; + p.immcount <- p.immcount + 1; + if not (p==e) then + (match !stack with [] -> assert false | _::s -> stack := s); + last_alloc := get_alloc (); + r + with reraise -> + let dw = spent_alloc () in + let dt = get_time () - t in + e.tottime <- e.tottime + dt; e.owntime <- e.owntime + dt; + ajoute_ownalloc e dw; + ajoute_totalloc e dw; + p.owntime <- p.owntime - dt; + ajoute_totalloc p (e.totalloc -. totalloc0); + p.intcount <- p.intcount + e.intcount - intcount0 + 1; + p.immcount <- p.immcount + 1; + if not (p==e) then + (match !stack with [] -> assert false | _::s -> stack := s); + last_alloc := get_alloc (); + raise reraise + +let profile6 e f a b c d g h = + let dw = spent_alloc () in + match !stack with [] -> assert false | p::_ -> + (* We add spent alloc since last measure to current caller own/total alloc *) + ajoute_ownalloc p dw; + ajoute_totalloc p dw; + e.owncount <- e.owncount + 1; + if not (p==e) then stack := e::!stack; + let totalloc0 = e.totalloc in + let intcount0 = e.intcount in + let t = get_time () in + try + last_alloc := get_alloc (); + let r = f a b c d g h in + let dw = spent_alloc () in + let dt = get_time () - t in + e.tottime <- e.tottime + dt; e.owntime <- e.owntime + dt; + ajoute_ownalloc e dw; + ajoute_totalloc e dw; + p.owntime <- p.owntime - dt; + ajoute_totalloc p (e.totalloc -. totalloc0); + p.intcount <- p.intcount + e.intcount - intcount0 + 1; + p.immcount <- p.immcount + 1; + if not (p==e) then + (match !stack with [] -> assert false | _::s -> stack := s); + last_alloc := get_alloc (); + r + with reraise -> + let dw = spent_alloc () in + let dt = get_time () - t in + e.tottime <- e.tottime + dt; e.owntime <- e.owntime + dt; + ajoute_ownalloc e dw; + ajoute_totalloc e dw; + p.owntime <- p.owntime - dt; + ajoute_totalloc p (e.totalloc -. totalloc0); + p.intcount <- p.intcount + e.intcount - intcount0 + 1; + p.immcount <- p.immcount + 1; + if not (p==e) then + (match !stack with [] -> assert false | _::s -> stack := s); + last_alloc := get_alloc (); + raise reraise + +let profile7 e f a b c d g h i = + let dw = spent_alloc () in + match !stack with [] -> assert false | p::_ -> + (* We add spent alloc since last measure to current caller own/total alloc *) + ajoute_ownalloc p dw; + ajoute_totalloc p dw; + e.owncount <- e.owncount + 1; + if not (p==e) then stack := e::!stack; + let totalloc0 = e.totalloc in + let intcount0 = e.intcount in + let t = get_time () in + try + last_alloc := get_alloc (); + let r = f a b c d g h i in + let dw = spent_alloc () in + let dt = get_time () - t in + e.tottime <- e.tottime + dt; e.owntime <- e.owntime + dt; + ajoute_ownalloc e dw; + ajoute_totalloc e dw; + p.owntime <- p.owntime - dt; + ajoute_totalloc p (e.totalloc -. totalloc0); + p.intcount <- p.intcount + e.intcount - intcount0 + 1; + p.immcount <- p.immcount + 1; + if not (p==e) then + (match !stack with [] -> assert false | _::s -> stack := s); + last_alloc := get_alloc (); + r + with reraise -> + let dw = spent_alloc () in + let dt = get_time () - t in + e.tottime <- e.tottime + dt; e.owntime <- e.owntime + dt; + ajoute_ownalloc e dw; + ajoute_totalloc e dw; + p.owntime <- p.owntime - dt; + ajoute_totalloc p (e.totalloc -. totalloc0); + p.intcount <- p.intcount + e.intcount - intcount0 + 1; + p.immcount <- p.immcount + 1; + if not (p==e) then + (match !stack with [] -> assert false | _::s -> stack := s); + last_alloc := get_alloc (); + raise reraise + +let profile8 e f a b c d g h i j = + let dw = spent_alloc () in + match !stack with [] -> assert false | p::_ -> + (* We add spent alloc since last measure to current caller own/total alloc *) + ajoute_ownalloc p dw; + ajoute_totalloc p dw; + e.owncount <- e.owncount + 1; + if not (p==e) then stack := e::!stack; + let totalloc0 = e.totalloc in + let intcount0 = e.intcount in + let t = get_time () in + try + last_alloc := get_alloc (); + let r = f a b c d g h i j in + let dw = spent_alloc () in + let dt = get_time () - t in + e.tottime <- e.tottime + dt; e.owntime <- e.owntime + dt; + ajoute_ownalloc e dw; + ajoute_totalloc e dw; + p.owntime <- p.owntime - dt; + ajoute_totalloc p (e.totalloc -. totalloc0); + p.intcount <- p.intcount + e.intcount - intcount0 + 1; + p.immcount <- p.immcount + 1; + if not (p==e) then + (match !stack with [] -> assert false | _::s -> stack := s); + last_alloc := get_alloc (); + r + with reraise -> + let dw = spent_alloc () in + let dt = get_time () - t in + e.tottime <- e.tottime + dt; e.owntime <- e.owntime + dt; + ajoute_ownalloc e dw; + ajoute_totalloc e dw; + p.owntime <- p.owntime - dt; + ajoute_totalloc p (e.totalloc -. totalloc0); + p.intcount <- p.intcount + e.intcount - intcount0 + 1; + p.immcount <- p.immcount + 1; + if not (p==e) then + (match !stack with [] -> assert false | _::s -> stack := s); + last_alloc := get_alloc (); + raise reraise + +let print_logical_stats a = + let (c, s, d) = CObj.obj_stats a in + Printf.printf "Expanded size: %10d (str: %8d) Depth: %6d\n" (s+c) c d + +let print_stats a = + let (c1, s, d) = CObj.obj_stats a in + let c2 = CObj.size a in + Printf.printf "Size: %8d (exp: %10d) Depth: %6d\n" + c2 (s + c1) d +(* +let _ = Gc.set { (Gc.get()) with Gc.verbose = 13 } +*) diff --git a/lib/cProfile.mli b/lib/cProfile.mli new file mode 100644 index 000000000..cae4397a1 --- /dev/null +++ b/lib/cProfile.mli @@ -0,0 +1,119 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* unit + +val print_profile : unit -> unit +val reset_profile : unit -> unit +val init_profile : unit -> unit +val declare_profile : string -> profile_key + +val profile1 : profile_key -> ('a -> 'b) -> 'a -> 'b +val profile2 : profile_key -> ('a -> 'b -> 'c) -> 'a -> 'b -> 'c +val profile3 : + profile_key -> ('a -> 'b -> 'c -> 'd) -> 'a -> 'b -> 'c -> 'd +val profile4 : + profile_key -> ('a -> 'b -> 'c -> 'd -> 'e) -> 'a -> 'b -> 'c -> 'd -> 'e +val profile5 : + profile_key -> + ('a -> 'b -> 'c -> 'd -> 'e -> 'f) -> 'a -> 'b -> 'c -> 'd -> 'e -> 'f +val profile6 : + profile_key -> + ('a -> 'b -> 'c -> 'd -> 'e -> 'f -> 'g) + -> 'a -> 'b -> 'c -> 'd -> 'e -> 'f -> 'g +val profile7 : + profile_key -> + ('a -> 'b -> 'c -> 'd -> 'e -> 'f -> 'g -> 'h) + -> 'a -> 'b -> 'c -> 'd -> 'e -> 'f -> 'g -> 'h +val profile8 : + profile_key -> + ('a -> 'b -> 'c -> 'd -> 'e -> 'f -> 'g -> 'h -> 'i) + -> 'a -> 'b -> 'c -> 'd -> 'e -> 'f -> 'g -> 'h -> 'i + + +(** Some utilities to compute the logical and physical sizes and depth + of ML objects *) + +(** Print logical size (in words) and depth of its argument + This function does not disturb the heap *) +val print_logical_stats : 'a -> unit + +(** Print physical size, logical size (in words) and depth of its argument + This function allocates itself a lot (the same order of magnitude + as the physical size of its argument) *) +val print_stats : 'a -> unit diff --git a/lib/lib.mllib b/lib/lib.mllib index 8791f0741..66f939a91 100644 --- a/lib/lib.mllib +++ b/lib/lib.mllib @@ -9,7 +9,7 @@ System CThread Spawn Trie -Profile +CProfile Explore Predicate Rtree diff --git a/lib/profile.ml b/lib/profile.ml deleted file mode 100644 index 0bc226a45..000000000 --- a/lib/profile.ml +++ /dev/null @@ -1,714 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* [] || Flags.profile then begin - let outside = create_record () in - stack := [outside]; - last_alloc := get_alloc (); - init_alloc := !last_alloc; - init_time := get_time (); - outside.tottime <- - !init_time; - outside.owntime <- - !init_time - end - -let ajoute n o = - o.owntime <- o.owntime + n.owntime; - o.tottime <- o.tottime + n.tottime; - ajoute_ownalloc o n.ownalloc; - ajoute_totalloc o n.totalloc; - o.owncount <- o.owncount + n.owncount; - o.intcount <- o.intcount + n.intcount; - o.immcount <- o.immcount + n.immcount - -let ajoute_to_list ((name,n) as e) l = - try ajoute n (List.assoc name l); l - with Not_found -> e::l - -let magic = 1249 - -let merge_profile filename (curr_table, curr_outside, curr_total as new_data) = - let (old_table, old_outside, old_total) = - try - let c = open_in filename in - if input_binary_int c <> magic - then Printf.printf "Incompatible recording file: %s\n" filename; - let old_data = input_value c in - close_in c; - old_data - with Sys_error msg -> - (Printf.printf "Unable to open %s: %s\n" filename msg; - new_data) in - let updated_data = - let updated_table = List.fold_right ajoute_to_list curr_table old_table in - ajoute curr_outside old_outside; - ajoute curr_total old_total; - (updated_table, old_outside, old_total) in - begin - (try - let c = - open_out_gen - [Open_creat;Open_wronly;Open_trunc;Open_binary] 0o644 filename in - output_binary_int c magic; - output_value c updated_data; - close_out c - with Sys_error _ -> Printf.printf "Unable to create recording file"); - updated_data - end - -(************************************************) -(* Compute a rough estimation of time overheads *) - -(* Time and space are not measured in the same way *) - -(* Byte allocation is an exact number and for long runs, the total - number of allocated bytes may exceed the maximum integer capacity - (2^31 on 32-bits architectures); therefore, allocation is measured - by small steps, total allocations are computed by adding elementary - measures and carries are controlled from step to step *) - -(* Unix measure of time is approximate and short delays are often - unperceivable; therefore, total times are measured in one (big) - step to avoid rounding errors and to get the best possible - approximation. - Note: Sys.time is the same as: - Unix.(let x = times () in x.tms_utime +. x.tms_stime) - *) - -(* ----------- start profile for f1 -overheadA| ... - ---------- [1w1] 1st call to get_time for f1 - overheadB| ... - ---------- start f1 - real 1 | ... - ---------- start profile for 1st call to f2 inside f1 - overheadA| ... - ---------- [2w1] 1st call to get_time for 1st f2 - overheadB| ... - ---------- start 1st f2 - real 2 | ... - ---------- end 1st f2 - overheadC| ... - ---------- [2w1] 2nd call to get_time for 1st f2 - overheadD| ... - ---------- end profile for 1st f2 - real 1 | ... - ---------- start profile for 2nd call to f2 inside f1 - overheadA| ... - ---------- [2'w1] 1st call to get_time for 2nd f2 - overheadB| ... - ---------- start 2nd f2 - real 2' | ... - ---------- end 2nd f2 - overheadC| ... - ---------- [2'w2] 2nd call to get_time for 2nd f2 - overheadD| ... - ---------- end profile for f2 - real 1 | ... - ---------- end f1 - overheadC| ... ----------- [1w1'] 2nd call to get_time for f1 -overheadD| ... ----------- end profile for f1 - -When profiling f2, overheadB + overheadC should be subtracted from measure -and overheadA + overheadB + overheadC + overheadD should be subtracted from -the amount for f1 - -Then the relevant overheads are : - - "overheadB + overheadC" to be subtracted to the measure of f as many time as f is called and - - "overheadA + overheadB + overheadC + overheadD" to be subtracted to - the measure of f as many time as f calls a profiled function (itself - included) -*) - -let dummy_last_alloc = ref 0.0 -let dummy_spent_alloc () = - let now = get_alloc () in - let before = !last_alloc in - last_alloc := now; - now -. before -let dummy_f x = x -let dummy_stack = ref [create_record ()] -let dummy_ov = 0 - -let loops = 10000 - -let time_overhead_A_D () = - let e = create_record () in - let before = get_time () in - for _i = 1 to loops do - (* This is a copy of profile1 for overhead estimation *) - let dw = dummy_spent_alloc () in - match !dummy_stack with [] -> assert false | p::_ -> - ajoute_ownalloc p dw; - ajoute_totalloc p dw; - e.owncount <- e.owncount + 1; - if not (p==e) then stack := e::!stack; - let totalloc0 = e.totalloc in - let intcount0 = e.intcount in - let dt = get_time () - 1 in - e.tottime <- dt + dummy_ov; e.owntime <- e.owntime + e.tottime; - ajoute_ownalloc p dw; - ajoute_totalloc p dw; - p.owntime <- p.owntime - e.tottime; - ajoute_totalloc p (e.totalloc-.totalloc0); - p.intcount <- p.intcount + e.intcount - intcount0 + 1; - p.immcount <- p.immcount + 1; - if not (p==e) then - (match !dummy_stack with [] -> assert false | _::s -> stack := s); - dummy_last_alloc := get_alloc () - done; - let after = get_time () in - let beforeloop = get_time () in - for _i = 1 to loops do () done; - let afterloop = get_time () in - float_of_int ((after - before) - (afterloop - beforeloop)) - /. float_of_int loops - -let time_overhead_B_C () = - let dummy_x = 0 in - let before = get_time () in - for _i = 1 to loops do - try - dummy_last_alloc := get_alloc (); - let _r = dummy_f dummy_x in - let _dw = dummy_spent_alloc () in - let _dt = get_time () in - () - with e when CErrors.noncritical e -> assert false - done; - let after = get_time () in - let beforeloop = get_time () in - for _i = 1 to loops do () done; - let afterloop = get_time () in - float_of_int ((after - before) - (afterloop - beforeloop)) - /. float_of_int loops - -let compute_alloc lo = lo /. (float_of_int word_length) - -(************************************************) -(* End a profiling session and print the result *) - -let format_profile (table, outside, total) = - print_newline (); - Printf.printf - "%-23s %9s %9s %10s %10s %10s\n" - "Function name" "Own time" "Tot. time" "Own alloc" "Tot. alloc" "Calls "; - let l = List.sort (fun (_,{tottime=p}) (_,{tottime=p'}) -> p' - p) table in - List.iter (fun (name,e) -> - Printf.printf - "%-23s %9.2f %9.2f %10.0f %10.0f %6d %6d\n" - name - (float_of_time e.owntime) (float_of_time e.tottime) - (compute_alloc e.ownalloc) - (compute_alloc e.totalloc) - e.owncount e.intcount) - l; - Printf.printf "%-23s %9.2f %9.2f %10.0f %10.0f %6d\n" - "others" - (float_of_time outside.owntime) (float_of_time outside.tottime) - (compute_alloc outside.ownalloc) - (compute_alloc outside.totalloc) - outside.intcount; - (* Here, own contains overhead time/alloc *) - Printf.printf "%-23s %9.2f %9.2f %10.0f %10.0f\n" - "Est. overhead/total" - (float_of_time total.owntime) (float_of_time total.tottime) - (compute_alloc total.ownalloc) - (compute_alloc total.totalloc); - Printf.printf - "Time in seconds and allocation in words (1 word = %d bytes)\n" - word_length - -let recording_file = ref "" -let set_recording s = recording_file := s - -let adjust_time ov_bc ov_ad e = - let bc_imm = float_of_int e.owncount *. ov_bc in - let ad_imm = float_of_int e.immcount *. ov_ad in - let abcd_all = float_of_int e.intcount *. (ov_ad +. ov_bc) in - {e with - tottime = e.tottime - int_of_float (abcd_all +. bc_imm); - owntime = e.owntime - int_of_float (ad_imm +. bc_imm) } - -let close_profile print = - if !prof_table <> [] then begin - let dw = spent_alloc () in - let t = get_time () in - match !stack with - | [outside] -> - outside.tottime <- outside.tottime + t; - outside.owntime <- outside.owntime + t; - ajoute_ownalloc outside dw; - ajoute_totalloc outside dw; - let ov_bc = time_overhead_B_C () (* B+C overhead *) in - let ov_ad = time_overhead_A_D () (* A+D overhead *) in - let adjust (n,e) = (n, adjust_time ov_bc ov_ad e) in - let adjtable = List.map adjust !prof_table in - let adjoutside = adjust_time ov_bc ov_ad outside in - let totalloc = !last_alloc -. !init_alloc in - let total = create_record () in - total.tottime <- outside.tottime; - total.totalloc <- totalloc; - (* We compute estimations of overhead, put into "own" fields *) - total.owntime <- outside.tottime - adjoutside.tottime; - total.ownalloc <- totalloc -. outside.totalloc; - let current_data = (adjtable, adjoutside, total) in - let updated_data = - match !recording_file with - | "" -> current_data - | name -> merge_profile !recording_file current_data - in - if print then format_profile updated_data; - init_profile () - | _ -> failwith "Inconsistency" - end - -let print_profile () = close_profile true - -let declare_profile name = - if name = "___outside___" || name = "___total___" then - failwith ("Error: "^name^" is a reserved keyword"); - let e = create_record () in - prof_table := (name,e)::!prof_table; - e - -(******************************) -(* Entry points for profiling *) -let profile1 e f a = - let dw = spent_alloc () in - match !stack with [] -> assert false | p::_ -> - (* We add spent alloc since last measure to current caller own/total alloc *) - ajoute_ownalloc p dw; - ajoute_totalloc p dw; - e.owncount <- e.owncount + 1; - if not (p==e) then stack := e::!stack; - let totalloc0 = e.totalloc in - let intcount0 = e.intcount in - let t = get_time () in - try - last_alloc := get_alloc (); - let r = f a in - let dw = spent_alloc () in - let dt = get_time () - t in - e.tottime <- e.tottime + dt; e.owntime <- e.owntime + dt; - ajoute_ownalloc e dw; - ajoute_totalloc e dw; - p.owntime <- p.owntime - dt; - ajoute_totalloc p (e.totalloc -. totalloc0); - p.intcount <- p.intcount + e.intcount - intcount0 + 1; - p.immcount <- p.immcount + 1; - if not (p==e) then - (match !stack with [] -> assert false | _::s -> stack := s); - last_alloc := get_alloc (); - r - with reraise -> - let dw = spent_alloc () in - let dt = get_time () - t in - e.tottime <- e.tottime + dt; e.owntime <- e.owntime + dt; - ajoute_ownalloc e dw; - ajoute_totalloc e dw; - p.owntime <- p.owntime - dt; - ajoute_totalloc p (e.totalloc -. totalloc0); - p.intcount <- p.intcount + e.intcount - intcount0 + 1; - p.immcount <- p.immcount + 1; - if not (p==e) then - (match !stack with [] -> assert false | _::s -> stack := s); - last_alloc := get_alloc (); - raise reraise - -let profile2 e f a b = - let dw = spent_alloc () in - match !stack with [] -> assert false | p::_ -> - (* We add spent alloc since last measure to current caller own/total alloc *) - ajoute_ownalloc p dw; - ajoute_totalloc p dw; - e.owncount <- e.owncount + 1; - if not (p==e) then stack := e::!stack; - let totalloc0 = e.totalloc in - let intcount0 = e.intcount in - let t = get_time () in - try - last_alloc := get_alloc (); - let r = f a b in - let dw = spent_alloc () in - let dt = get_time () - t in - e.tottime <- e.tottime + dt; e.owntime <- e.owntime + dt; - ajoute_ownalloc e dw; - ajoute_totalloc e dw; - p.owntime <- p.owntime - dt; - ajoute_totalloc p (e.totalloc -. totalloc0); - p.intcount <- p.intcount + e.intcount - intcount0 + 1; - p.immcount <- p.immcount + 1; - if not (p==e) then - (match !stack with [] -> assert false | _::s -> stack := s); - last_alloc := get_alloc (); - r - with reraise -> - let dw = spent_alloc () in - let dt = get_time () - t in - e.tottime <- e.tottime + dt; e.owntime <- e.owntime + dt; - ajoute_ownalloc e dw; - ajoute_totalloc e dw; - p.owntime <- p.owntime - dt; - ajoute_totalloc p (e.totalloc -. totalloc0); - p.intcount <- p.intcount + e.intcount - intcount0 + 1; - p.immcount <- p.immcount + 1; - if not (p==e) then - (match !stack with [] -> assert false | _::s -> stack := s); - last_alloc := get_alloc (); - raise reraise - -let profile3 e f a b c = - let dw = spent_alloc () in - match !stack with [] -> assert false | p::_ -> - (* We add spent alloc since last measure to current caller own/total alloc *) - ajoute_ownalloc p dw; - ajoute_totalloc p dw; - e.owncount <- e.owncount + 1; - if not (p==e) then stack := e::!stack; - let totalloc0 = e.totalloc in - let intcount0 = e.intcount in - let t = get_time () in - try - last_alloc := get_alloc (); - let r = f a b c in - let dw = spent_alloc () in - let dt = get_time () - t in - e.tottime <- e.tottime + dt; e.owntime <- e.owntime + dt; - ajoute_ownalloc e dw; - ajoute_totalloc e dw; - p.owntime <- p.owntime - dt; - ajoute_totalloc p (e.totalloc -. totalloc0); - p.intcount <- p.intcount + e.intcount - intcount0 + 1; - p.immcount <- p.immcount + 1; - if not (p==e) then - (match !stack with [] -> assert false | _::s -> stack := s); - last_alloc := get_alloc (); - r - with reraise -> - let dw = spent_alloc () in - let dt = get_time () - t in - e.tottime <- e.tottime + dt; e.owntime <- e.owntime + dt; - ajoute_ownalloc e dw; - ajoute_totalloc e dw; - p.owntime <- p.owntime - dt; - ajoute_totalloc p (e.totalloc -. totalloc0); - p.intcount <- p.intcount + e.intcount - intcount0 + 1; - p.immcount <- p.immcount + 1; - if not (p==e) then - (match !stack with [] -> assert false | _::s -> stack := s); - last_alloc := get_alloc (); - raise reraise - -let profile4 e f a b c d = - let dw = spent_alloc () in - match !stack with [] -> assert false | p::_ -> - (* We add spent alloc since last measure to current caller own/total alloc *) - ajoute_ownalloc p dw; - ajoute_totalloc p dw; - e.owncount <- e.owncount + 1; - if not (p==e) then stack := e::!stack; - let totalloc0 = e.totalloc in - let intcount0 = e.intcount in - let t = get_time () in - try - last_alloc := get_alloc (); - let r = f a b c d in - let dw = spent_alloc () in - let dt = get_time () - t in - e.tottime <- e.tottime + dt; e.owntime <- e.owntime + dt; - ajoute_ownalloc e dw; - ajoute_totalloc e dw; - p.owntime <- p.owntime - dt; - ajoute_totalloc p (e.totalloc -. totalloc0); - p.intcount <- p.intcount + e.intcount - intcount0 + 1; - p.immcount <- p.immcount + 1; - if not (p==e) then - (match !stack with [] -> assert false | _::s -> stack := s); - last_alloc := get_alloc (); - r - with reraise -> - let dw = spent_alloc () in - let dt = get_time () - t in - e.tottime <- e.tottime + dt; e.owntime <- e.owntime + dt; - ajoute_ownalloc e dw; - ajoute_totalloc e dw; - p.owntime <- p.owntime - dt; - ajoute_totalloc p (e.totalloc -. totalloc0); - p.intcount <- p.intcount + e.intcount - intcount0 + 1; - p.immcount <- p.immcount + 1; - if not (p==e) then - (match !stack with [] -> assert false | _::s -> stack := s); - last_alloc := get_alloc (); - raise reraise - -let profile5 e f a b c d g = - let dw = spent_alloc () in - match !stack with [] -> assert false | p::_ -> - (* We add spent alloc since last measure to current caller own/total alloc *) - ajoute_ownalloc p dw; - ajoute_totalloc p dw; - e.owncount <- e.owncount + 1; - if not (p==e) then stack := e::!stack; - let totalloc0 = e.totalloc in - let intcount0 = e.intcount in - let t = get_time () in - try - last_alloc := get_alloc (); - let r = f a b c d g in - let dw = spent_alloc () in - let dt = get_time () - t in - e.tottime <- e.tottime + dt; e.owntime <- e.owntime + dt; - ajoute_ownalloc e dw; - ajoute_totalloc e dw; - p.owntime <- p.owntime - dt; - ajoute_totalloc p (e.totalloc -. totalloc0); - p.intcount <- p.intcount + e.intcount - intcount0 + 1; - p.immcount <- p.immcount + 1; - if not (p==e) then - (match !stack with [] -> assert false | _::s -> stack := s); - last_alloc := get_alloc (); - r - with reraise -> - let dw = spent_alloc () in - let dt = get_time () - t in - e.tottime <- e.tottime + dt; e.owntime <- e.owntime + dt; - ajoute_ownalloc e dw; - ajoute_totalloc e dw; - p.owntime <- p.owntime - dt; - ajoute_totalloc p (e.totalloc -. totalloc0); - p.intcount <- p.intcount + e.intcount - intcount0 + 1; - p.immcount <- p.immcount + 1; - if not (p==e) then - (match !stack with [] -> assert false | _::s -> stack := s); - last_alloc := get_alloc (); - raise reraise - -let profile6 e f a b c d g h = - let dw = spent_alloc () in - match !stack with [] -> assert false | p::_ -> - (* We add spent alloc since last measure to current caller own/total alloc *) - ajoute_ownalloc p dw; - ajoute_totalloc p dw; - e.owncount <- e.owncount + 1; - if not (p==e) then stack := e::!stack; - let totalloc0 = e.totalloc in - let intcount0 = e.intcount in - let t = get_time () in - try - last_alloc := get_alloc (); - let r = f a b c d g h in - let dw = spent_alloc () in - let dt = get_time () - t in - e.tottime <- e.tottime + dt; e.owntime <- e.owntime + dt; - ajoute_ownalloc e dw; - ajoute_totalloc e dw; - p.owntime <- p.owntime - dt; - ajoute_totalloc p (e.totalloc -. totalloc0); - p.intcount <- p.intcount + e.intcount - intcount0 + 1; - p.immcount <- p.immcount + 1; - if not (p==e) then - (match !stack with [] -> assert false | _::s -> stack := s); - last_alloc := get_alloc (); - r - with reraise -> - let dw = spent_alloc () in - let dt = get_time () - t in - e.tottime <- e.tottime + dt; e.owntime <- e.owntime + dt; - ajoute_ownalloc e dw; - ajoute_totalloc e dw; - p.owntime <- p.owntime - dt; - ajoute_totalloc p (e.totalloc -. totalloc0); - p.intcount <- p.intcount + e.intcount - intcount0 + 1; - p.immcount <- p.immcount + 1; - if not (p==e) then - (match !stack with [] -> assert false | _::s -> stack := s); - last_alloc := get_alloc (); - raise reraise - -let profile7 e f a b c d g h i = - let dw = spent_alloc () in - match !stack with [] -> assert false | p::_ -> - (* We add spent alloc since last measure to current caller own/total alloc *) - ajoute_ownalloc p dw; - ajoute_totalloc p dw; - e.owncount <- e.owncount + 1; - if not (p==e) then stack := e::!stack; - let totalloc0 = e.totalloc in - let intcount0 = e.intcount in - let t = get_time () in - try - last_alloc := get_alloc (); - let r = f a b c d g h i in - let dw = spent_alloc () in - let dt = get_time () - t in - e.tottime <- e.tottime + dt; e.owntime <- e.owntime + dt; - ajoute_ownalloc e dw; - ajoute_totalloc e dw; - p.owntime <- p.owntime - dt; - ajoute_totalloc p (e.totalloc -. totalloc0); - p.intcount <- p.intcount + e.intcount - intcount0 + 1; - p.immcount <- p.immcount + 1; - if not (p==e) then - (match !stack with [] -> assert false | _::s -> stack := s); - last_alloc := get_alloc (); - r - with reraise -> - let dw = spent_alloc () in - let dt = get_time () - t in - e.tottime <- e.tottime + dt; e.owntime <- e.owntime + dt; - ajoute_ownalloc e dw; - ajoute_totalloc e dw; - p.owntime <- p.owntime - dt; - ajoute_totalloc p (e.totalloc -. totalloc0); - p.intcount <- p.intcount + e.intcount - intcount0 + 1; - p.immcount <- p.immcount + 1; - if not (p==e) then - (match !stack with [] -> assert false | _::s -> stack := s); - last_alloc := get_alloc (); - raise reraise - -let profile8 e f a b c d g h i j = - let dw = spent_alloc () in - match !stack with [] -> assert false | p::_ -> - (* We add spent alloc since last measure to current caller own/total alloc *) - ajoute_ownalloc p dw; - ajoute_totalloc p dw; - e.owncount <- e.owncount + 1; - if not (p==e) then stack := e::!stack; - let totalloc0 = e.totalloc in - let intcount0 = e.intcount in - let t = get_time () in - try - last_alloc := get_alloc (); - let r = f a b c d g h i j in - let dw = spent_alloc () in - let dt = get_time () - t in - e.tottime <- e.tottime + dt; e.owntime <- e.owntime + dt; - ajoute_ownalloc e dw; - ajoute_totalloc e dw; - p.owntime <- p.owntime - dt; - ajoute_totalloc p (e.totalloc -. totalloc0); - p.intcount <- p.intcount + e.intcount - intcount0 + 1; - p.immcount <- p.immcount + 1; - if not (p==e) then - (match !stack with [] -> assert false | _::s -> stack := s); - last_alloc := get_alloc (); - r - with reraise -> - let dw = spent_alloc () in - let dt = get_time () - t in - e.tottime <- e.tottime + dt; e.owntime <- e.owntime + dt; - ajoute_ownalloc e dw; - ajoute_totalloc e dw; - p.owntime <- p.owntime - dt; - ajoute_totalloc p (e.totalloc -. totalloc0); - p.intcount <- p.intcount + e.intcount - intcount0 + 1; - p.immcount <- p.immcount + 1; - if not (p==e) then - (match !stack with [] -> assert false | _::s -> stack := s); - last_alloc := get_alloc (); - raise reraise - -let print_logical_stats a = - let (c, s, d) = CObj.obj_stats a in - Printf.printf "Expanded size: %10d (str: %8d) Depth: %6d\n" (s+c) c d - -let print_stats a = - let (c1, s, d) = CObj.obj_stats a in - let c2 = CObj.size a in - Printf.printf "Size: %8d (exp: %10d) Depth: %6d\n" - c2 (s + c1) d -(* -let _ = Gc.set { (Gc.get()) with Gc.verbose = 13 } -*) diff --git a/lib/profile.mli b/lib/profile.mli deleted file mode 100644 index cae4397a1..000000000 --- a/lib/profile.mli +++ /dev/null @@ -1,119 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* unit - -val print_profile : unit -> unit -val reset_profile : unit -> unit -val init_profile : unit -> unit -val declare_profile : string -> profile_key - -val profile1 : profile_key -> ('a -> 'b) -> 'a -> 'b -val profile2 : profile_key -> ('a -> 'b -> 'c) -> 'a -> 'b -> 'c -val profile3 : - profile_key -> ('a -> 'b -> 'c -> 'd) -> 'a -> 'b -> 'c -> 'd -val profile4 : - profile_key -> ('a -> 'b -> 'c -> 'd -> 'e) -> 'a -> 'b -> 'c -> 'd -> 'e -val profile5 : - profile_key -> - ('a -> 'b -> 'c -> 'd -> 'e -> 'f) -> 'a -> 'b -> 'c -> 'd -> 'e -> 'f -val profile6 : - profile_key -> - ('a -> 'b -> 'c -> 'd -> 'e -> 'f -> 'g) - -> 'a -> 'b -> 'c -> 'd -> 'e -> 'f -> 'g -val profile7 : - profile_key -> - ('a -> 'b -> 'c -> 'd -> 'e -> 'f -> 'g -> 'h) - -> 'a -> 'b -> 'c -> 'd -> 'e -> 'f -> 'g -> 'h -val profile8 : - profile_key -> - ('a -> 'b -> 'c -> 'd -> 'e -> 'f -> 'g -> 'h -> 'i) - -> 'a -> 'b -> 'c -> 'd -> 'e -> 'f -> 'g -> 'h -> 'i - - -(** Some utilities to compute the logical and physical sizes and depth - of ML objects *) - -(** Print logical size (in words) and depth of its argument - This function does not disturb the heap *) -val print_logical_stats : 'a -> unit - -(** Print physical size, logical size (in words) and depth of its argument - This function allocates itself a lot (the same order of magnitude - as the physical size of its argument) *) -val print_stats : 'a -> unit diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml index c0060c5a7..ee34161dd 100644 --- a/plugins/ltac/rewrite.ml +++ b/plugins/ltac/rewrite.ml @@ -361,8 +361,8 @@ end) = struct end (* let my_type_of env evars c = Typing.e_type_of env evars c *) -(* let mytypeofkey = Profile.declare_profile "my_type_of";; *) -(* let my_type_of = Profile.profile3 mytypeofkey my_type_of *) +(* let mytypeofkey = CProfile.declare_profile "my_type_of";; *) +(* let my_type_of = CProfile.profile3 mytypeofkey my_type_of *) let type_app_poly env env evd f args = @@ -2084,8 +2084,8 @@ let get_hyp gl (c,l) clause l2r = let general_rewrite_flags = { under_lambdas = false; on_morphisms = true } -(* let rewriteclaustac_key = Profile.declare_profile "cl_rewrite_clause_tac";; *) -(* let cl_rewrite_clause_tac = Profile.profile5 rewriteclaustac_key cl_rewrite_clause_tac *) +(* let rewriteclaustac_key = CProfile.declare_profile "cl_rewrite_clause_tac";; *) +(* let cl_rewrite_clause_tac = CProfile.profile5 rewriteclaustac_key cl_rewrite_clause_tac *) (** Setoid rewriting when called with "rewrite" *) let general_s_rewrite cl l2r occs (c,l) ~new_goals = diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml index e5776d2ec..cb8844623 100644 --- a/pretyping/evarconv.ml +++ b/pretyping/evarconv.ml @@ -1063,8 +1063,8 @@ let evar_conv_x ts = evar_conv_x (ts, true) (* Profiling *) let evar_conv_x = if Flags.profile then - let evar_conv_xkey = Profile.declare_profile "evar_conv_x" in - Profile.profile6 evar_conv_xkey evar_conv_x + let evar_conv_xkey = CProfile.declare_profile "evar_conv_x" in + CProfile.profile6 evar_conv_xkey evar_conv_x else evar_conv_x let evar_conv_hook_get, evar_conv_hook_set = Hook.make ~default:evar_conv_x () diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml index 2f8e5b964..30fc5f321 100644 --- a/pretyping/reductionops.ml +++ b/pretyping/reductionops.ml @@ -1269,11 +1269,11 @@ let nf_all env sigma = (* Conversion *) (********************************************************************) (* -let fkey = Profile.declare_profile "fhnf";; -let fhnf info v = Profile.profile2 fkey fhnf info v;; +let fkey = CProfile.declare_profile "fhnf";; +let fhnf info v = CProfile.profile2 fkey fhnf info v;; -let fakey = Profile.declare_profile "fhnf_apply";; -let fhnf_apply info k h a = Profile.profile4 fakey fhnf_apply info k h a;; +let fakey = CProfile.declare_profile "fhnf_apply";; +let fhnf_apply info k h a = CProfile.profile4 fakey fhnf_apply info k h a;; *) let is_transparent e k = diff --git a/pretyping/retyping.ml b/pretyping/retyping.ml index f8f086fad..00b175c48 100644 --- a/pretyping/retyping.ml +++ b/pretyping/retyping.ml @@ -227,8 +227,8 @@ let type_of_global_reference_knowing_conclusion env sigma c conclty = (* let f,_,_,_ = retype ~polyprop sigma in *) (* if lax then f env c else anomaly_on_error (f env) c *) -(* let get_type_of_key = Profile.declare_profile "get_type_of" *) -(* let get_type_of = Profile.profile5 get_type_of_key get_type_of *) +(* let get_type_of_key = CProfile.declare_profile "get_type_of" *) +(* let get_type_of = CProfile.profile5 get_type_of_key get_type_of *) (* let get_type_of ?(polyprop=true) ?(lax=false) env sigma c = *) (* get_type_of polyprop lax env sigma c *) diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml index 85383ba39..5a522e06a 100644 --- a/pretyping/tacred.ml +++ b/pretyping/tacred.ml @@ -927,8 +927,8 @@ let whd_simpl_orelse_delta_but_fix_old env sigma c = let whd_simpl_stack = if Flags.profile then - let key = Profile.declare_profile "whd_simpl_stack" in - Profile.profile3 key whd_simpl_stack + let key = CProfile.declare_profile "whd_simpl_stack" in + CProfile.profile3 key whd_simpl_stack else whd_simpl_stack (* Same as [whd_simpl] but also reduces constants that do not hide a diff --git a/pretyping/typeclasses.ml b/pretyping/typeclasses.ml index 2e213a51d..b49da57a4 100644 --- a/pretyping/typeclasses.ml +++ b/pretyping/typeclasses.ml @@ -552,8 +552,8 @@ let solve_all_instances env evd filter unique split fail = Hook.get get_solve_all_instances env evd filter unique split fail (** Profiling resolution of typeclasses *) -(* let solve_classeskey = Profile.declare_profile "solve_typeclasses" *) -(* let solve_problem = Profile.profile5 solve_classeskey solve_problem *) +(* let solve_classeskey = CProfile.declare_profile "solve_typeclasses" *) +(* let solve_problem = CProfile.profile5 solve_classeskey solve_problem *) let resolve_typeclasses ?(fast_path = true) ?(filter=no_goals) ?(unique=get_typeclasses_unique_solutions ()) ?(split=true) ?(fail=true) env evd = diff --git a/pretyping/unification.ml b/pretyping/unification.ml index 84ffab426..08329391d 100644 --- a/pretyping/unification.ml +++ b/pretyping/unification.ml @@ -2015,8 +2015,8 @@ let w_unify env evd cv_pb flags ty1 ty2 = let w_unify = if Flags.profile then - let wunifkey = Profile.declare_profile "w_unify" in - Profile.profile6 wunifkey w_unify + let wunifkey = CProfile.declare_profile "w_unify" in + CProfile.profile6 wunifkey w_unify else w_unify let w_unify env evd cv_pb ?(flags=default_unify_flags ()) ty1 ty2 = diff --git a/proofs/refiner.ml b/proofs/refiner.ml index 3e3313eb5..cd2b10906 100644 --- a/proofs/refiner.ml +++ b/proofs/refiner.ml @@ -30,8 +30,8 @@ let refiner pr goal_sigma = (* Profiling refiner *) let refiner = if Flags.profile then - let refiner_key = Profile.declare_profile "refiner" in - Profile.profile2 refiner_key refiner + let refiner_key = CProfile.declare_profile "refiner" in + CProfile.profile2 refiner_key refiner else refiner (*********************) diff --git a/tactics/auto.ml b/tactics/auto.ml index fa8435d1f..e7e21b5f4 100644 --- a/tactics/auto.ml +++ b/tactics/auto.ml @@ -514,8 +514,8 @@ let delta_auto debug mod_delta n lems dbnames = let delta_auto = if Flags.profile then - let key = Profile.declare_profile "delta_auto" in - Profile.profile5 key delta_auto + let key = CProfile.declare_profile "delta_auto" in + CProfile.profile5 key delta_auto else delta_auto let auto ?(debug=Off) n = delta_auto debug false n diff --git a/tactics/eauto.ml b/tactics/eauto.ml index f5c6ab879..b5cfbe68b 100644 --- a/tactics/eauto.ml +++ b/tactics/eauto.ml @@ -405,8 +405,8 @@ let e_search_auto debug (in_depth,p) lems db_list gl = pr_info_nop d; user_err Pp.(str "eauto: search failed") -(* let e_search_auto_key = Profile.declare_profile "e_search_auto" *) -(* let e_search_auto = Profile.profile5 e_search_auto_key e_search_auto *) +(* let e_search_auto_key = CProfile.declare_profile "e_search_auto" *) +(* let e_search_auto = CProfile.profile5 e_search_auto_key e_search_auto *) let eauto_with_bases ?(debug=Off) np lems db_list = tclTRY (e_search_auto debug np lems db_list) diff --git a/tactics/tactics.ml b/tactics/tactics.ml index e072bd95f..cb2a77558 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -1976,11 +1976,11 @@ let cut_and_apply c = (* Exact tactics *) (********************************************************************) -(* let convert_leqkey = Profile.declare_profile "convert_leq";; *) -(* let convert_leq = Profile.profile3 convert_leqkey convert_leq *) +(* let convert_leqkey = CProfile.declare_profile "convert_leq";; *) +(* let convert_leq = CProfile.profile3 convert_leqkey convert_leq *) -(* let refine_no_checkkey = Profile.declare_profile "refine_no_check";; *) -(* let refine_no_check = Profile.profile2 refine_no_checkkey refine_no_check *) +(* let refine_no_checkkey = CProfile.declare_profile "refine_no_check";; *) +(* let refine_no_check = CProfile.profile2 refine_no_checkkey refine_no_check *) let exact_no_check c = Refine.refine ~typecheck:false (fun h -> (h,c)) diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml index 553da2dc0..b62396317 100644 --- a/toplevel/coqtop.ml +++ b/toplevel/coqtop.ml @@ -756,7 +756,7 @@ let init_toplevel arglist = (* Coq's init process, phase 1: - OCaml parameters, and basic structures and IO *) - Profile.init_profile (); + CProfile.init_profile (); init_gc (); Sys.catch_break false; (* Ctrl-C is fatal during the initialisation *) let init_feeder = Feedback.add_feeder coqtop_init_feed in @@ -846,7 +846,7 @@ let start () = let sigma, env = Pfedit.get_current_context () in Feedback.msg_notice (Flags.(with_option raw_print (Prettyp.print_full_pure_context env) sigma) ++ fnl ()) end; - Profile.print_profile (); + CProfile.print_profile (); exit 0 (* [Coqtop.start] will be called by the code produced by coqmktop *) -- cgit v1.2.3