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`.
---
 lib/cProfile.ml  | 714 +++++++++++++++++++++++++++++++++++++++++++++++++++++++
 lib/cProfile.mli | 119 ++++++++++
 lib/lib.mllib    |   2 +-
 lib/profile.ml   | 714 -------------------------------------------------------
 lib/profile.mli  | 119 ----------
 5 files changed, 834 insertions(+), 834 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

(limited to 'lib')

diff --git a/lib/cProfile.ml b/lib/cProfile.ml
new file mode 100644
index 0000000000..0bc226a450
--- /dev/null
+++ b/lib/cProfile.ml
@@ -0,0 +1,714 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+let word_length = Sys.word_size / 8
+
+let float_of_time t = float_of_int t /. 100.
+let time_of_float f = int_of_float (f *. 100.)
+
+let get_time () =
+  time_of_float (Sys.time ())
+
+(* Since ocaml 3.01, gc statistics are in float *)
+let get_alloc () =
+  (* If you are unlucky, a minor collection can occur between the *)
+  (* measurements and produces allocation; we trigger a minor *)
+  (* collection in advance to be sure the measure is not corrupted *)
+  Gc.minor ();
+  Gc.allocated_bytes ()
+
+(* Rem: overhead was 16 bytes in ocaml 3.00 (long int) *)
+(* Rem: overhead is 100 bytes in ocaml 3.01 (double) *)
+
+let get_alloc_overhead =
+  let mark1 = get_alloc () in
+  let mark2 = get_alloc () in
+  let mark3 = get_alloc () in
+  (* If you are unlucky, a major collection can occur between the *)
+  (* measurements; with two measures the risk decreases *)
+  min (mark2 -. mark1) (mark3 -. mark2)
+
+let last_alloc = ref 0.0 (* set by init_profile () *)
+
+let spent_alloc () =
+  let now = get_alloc () in
+  let before = !last_alloc in
+  last_alloc := now;
+  now -. before -. get_alloc_overhead
+
+(* Profile records *)
+
+type profile_key = {
+  mutable owntime : int;
+  mutable tottime : int;
+  mutable ownalloc : float;
+  mutable totalloc : float;
+  mutable owncount : int;
+  mutable intcount : int;
+  mutable immcount : int;
+}
+
+let create_record () = {
+  owntime=0;
+  tottime=0;
+  ownalloc=0.0;
+  totalloc=0.0;
+  owncount=0;
+  intcount=0;
+  immcount=0
+}
+
+let ajoute_totalloc e dw = e.totalloc <- e.totalloc +. dw
+let ajoute_ownalloc e dw = e.ownalloc <- e.ownalloc +. dw
+
+let reset_record (n,e) =
+  e.owntime <- 0;
+  e.tottime <- 0;
+  e.ownalloc <- 0.0;
+  e.totalloc <- 0.0;
+  e.owncount <- 0;
+  e.intcount <- 0;
+  e.immcount <- 0
+
+(* Profile tables *)
+
+let prof_table = ref []
+let stack = ref []
+let init_time = ref 0
+let init_alloc = ref 0.0
+
+let reset_profile () = List.iter reset_record !prof_table
+
+let init_profile () =
+  (* We test Flags.profile as a way to support declaring profiled
+     functions in plugins *)
+  if !prof_table <> [] || 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 0000000000..cae4397a11
--- /dev/null
+++ b/lib/cProfile.mli
@@ -0,0 +1,119 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+(** {6 This program is a small time and allocation profiler for Objective Caml } *)
+
+(** Adapted from Christophe Raffalli *)
+
+(** To use it, link it with the program you want to profile.
+
+To trace a function "f" you first need to get a key for it by using :
+
+let fkey = declare_profile "f";;
+
+(the string is used to print the profile infomation). Warning: this
+function does a side effect. Choose the ident you want instead "fkey".
+
+Then if the function has ONE argument add the following just after
+the definition of "f" or just after the declare_profile if this one
+follows the definition of f.
+
+let f = profile1 fkey f;;
+
+If f has two arguments do the same with profile2, idem with 3, ...
+For more arguments than provided in this module, make a new copy of
+function profile and adapt for the needed arity.
+
+If you want to profile two mutually recursive functions, you had better
+to rename them :
+
+let fkey = declare_profile "f";;
+let gkey = declare_profile "g";;
+let f' = .... f' ... g'
+and g' = .... f' .... g'
+;;
+
+let f = profile fkey f';;
+let g = profile gkey g';;
+
+Before the program quits, you should call "print_profile ();;". It
+produces a result of the following kind:
+
+Function name              Own time Total time  Own alloc Tot. alloc     Calls
+f                            0.28      0.47        116        116      5      4
+h                            0.19      0.19          0          0      4      0
+g                            0.00      0.00          0          0      0      0
+others                       0.00      0.47        392        508             9
+Est. overhead/total          0.00      0.47       2752       3260
+
+- The first column is the name of the function.
+- The third column give the time (utime + stime) spent inside the function.
+- The second column give the time spend inside the function minus the
+  time spend in other profiled functions called by it
+- The 4th and 5th columns give the same for allocated words
+- The 6th and 7th columns give the number of calls to the function and
+  the number of calls to profiled functions inside the scope of the
+  current function
+
+Remarks:
+
+- If a function has a polymorphic type, you need to supply it with at
+  least one argument as in "let f a = profile1 fkey f a;;" (instead of
+  "let f = profile1 fkey f;;") in order to get generalization of the
+  type.
+- Each line of the form "let f a = profile1 fkey f a;;" in your code
+  counts for 5 words and each line of the form "let f
+  = profile1 fkey f;;" counts for 6 words (a word is 4 or 8 bytes
+  according to the architecture); this is counted for "others".
+- Time fields for functions doing a little job is usually non pertinent.
+
+i*)
+
+type profile_key
+
+val set_recording : string -> 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 8791f07417..66f939a910 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 0bc226a450..0000000000
--- a/lib/profile.ml
+++ /dev/null
@@ -1,714 +0,0 @@
-(************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017     *)
-(*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
-(************************************************************************)
-
-let word_length = Sys.word_size / 8
-
-let float_of_time t = float_of_int t /. 100.
-let time_of_float f = int_of_float (f *. 100.)
-
-let get_time () =
-  time_of_float (Sys.time ())
-
-(* Since ocaml 3.01, gc statistics are in float *)
-let get_alloc () =
-  (* If you are unlucky, a minor collection can occur between the *)
-  (* measurements and produces allocation; we trigger a minor *)
-  (* collection in advance to be sure the measure is not corrupted *)
-  Gc.minor ();
-  Gc.allocated_bytes ()
-
-(* Rem: overhead was 16 bytes in ocaml 3.00 (long int) *)
-(* Rem: overhead is 100 bytes in ocaml 3.01 (double) *)
-
-let get_alloc_overhead =
-  let mark1 = get_alloc () in
-  let mark2 = get_alloc () in
-  let mark3 = get_alloc () in
-  (* If you are unlucky, a major collection can occur between the *)
-  (* measurements; with two measures the risk decreases *)
-  min (mark2 -. mark1) (mark3 -. mark2)
-
-let last_alloc = ref 0.0 (* set by init_profile () *)
-
-let spent_alloc () =
-  let now = get_alloc () in
-  let before = !last_alloc in
-  last_alloc := now;
-  now -. before -. get_alloc_overhead
-
-(* Profile records *)
-
-type profile_key = {
-  mutable owntime : int;
-  mutable tottime : int;
-  mutable ownalloc : float;
-  mutable totalloc : float;
-  mutable owncount : int;
-  mutable intcount : int;
-  mutable immcount : int;
-}
-
-let create_record () = {
-  owntime=0;
-  tottime=0;
-  ownalloc=0.0;
-  totalloc=0.0;
-  owncount=0;
-  intcount=0;
-  immcount=0
-}
-
-let ajoute_totalloc e dw = e.totalloc <- e.totalloc +. dw
-let ajoute_ownalloc e dw = e.ownalloc <- e.ownalloc +. dw
-
-let reset_record (n,e) =
-  e.owntime <- 0;
-  e.tottime <- 0;
-  e.ownalloc <- 0.0;
-  e.totalloc <- 0.0;
-  e.owncount <- 0;
-  e.intcount <- 0;
-  e.immcount <- 0
-
-(* Profile tables *)
-
-let prof_table = ref []
-let stack = ref []
-let init_time = ref 0
-let init_alloc = ref 0.0
-
-let reset_profile () = List.iter reset_record !prof_table
-
-let init_profile () =
-  (* We test Flags.profile as a way to support declaring profiled
-     functions in plugins *)
-  if !prof_table <> [] || 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 cae4397a11..0000000000
--- a/lib/profile.mli
+++ /dev/null
@@ -1,119 +0,0 @@
-(************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017     *)
-(*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
-(************************************************************************)
-
-(** {6 This program is a small time and allocation profiler for Objective Caml } *)
-
-(** Adapted from Christophe Raffalli *)
-
-(** To use it, link it with the program you want to profile.
-
-To trace a function "f" you first need to get a key for it by using :
-
-let fkey = declare_profile "f";;
-
-(the string is used to print the profile infomation). Warning: this
-function does a side effect. Choose the ident you want instead "fkey".
-
-Then if the function has ONE argument add the following just after
-the definition of "f" or just after the declare_profile if this one
-follows the definition of f.
-
-let f = profile1 fkey f;;
-
-If f has two arguments do the same with profile2, idem with 3, ...
-For more arguments than provided in this module, make a new copy of
-function profile and adapt for the needed arity.
-
-If you want to profile two mutually recursive functions, you had better
-to rename them :
-
-let fkey = declare_profile "f";;
-let gkey = declare_profile "g";;
-let f' = .... f' ... g'
-and g' = .... f' .... g'
-;;
-
-let f = profile fkey f';;
-let g = profile gkey g';;
-
-Before the program quits, you should call "print_profile ();;". It
-produces a result of the following kind:
-
-Function name              Own time Total time  Own alloc Tot. alloc     Calls
-f                            0.28      0.47        116        116      5      4
-h                            0.19      0.19          0          0      4      0
-g                            0.00      0.00          0          0      0      0
-others                       0.00      0.47        392        508             9
-Est. overhead/total          0.00      0.47       2752       3260
-
-- The first column is the name of the function.
-- The third column give the time (utime + stime) spent inside the function.
-- The second column give the time spend inside the function minus the
-  time spend in other profiled functions called by it
-- The 4th and 5th columns give the same for allocated words
-- The 6th and 7th columns give the number of calls to the function and
-  the number of calls to profiled functions inside the scope of the
-  current function
-
-Remarks:
-
-- If a function has a polymorphic type, you need to supply it with at
-  least one argument as in "let f a = profile1 fkey f a;;" (instead of
-  "let f = profile1 fkey f;;") in order to get generalization of the
-  type.
-- Each line of the form "let f a = profile1 fkey f a;;" in your code
-  counts for 5 words and each line of the form "let f
-  = profile1 fkey f;;" counts for 6 words (a word is 4 or 8 bytes
-  according to the architecture); this is counted for "others".
-- Time fields for functions doing a little job is usually non pertinent.
-
-i*)
-
-type profile_key
-
-val set_recording : string -> 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
-- 
cgit v1.2.3