From 51b32595081d279624c8ec162f9ed686ed660d9b Mon Sep 17 00:00:00 2001
From: Jason Gross
Date: Wed, 11 May 2016 12:30:15 -0400
Subject: Remove a spurious tclFINALLY when not profiling

Implement the suggestion of @mattam82 to check whether or not we're
profiling before inserting the tclFINALLY.

Timing stats:

Using:
```bash
make clean && git clean -xfd && ./configure -local -with-doc no -coqide no && /usr/bin/time -f "all coq (real: %e, user: %U, sys: %S, mem: %M ko)" make STDTIME='/usr/bin/time -f "$* (real: %e, user: %U, sys: %S, mem: %M ko)"' TIMED=1 -j4 2>&1
```

Without LtacProf (4c078b0362542908eb2fe1d63f0d867b339953fd), two runs:
```
real: 147.96, user: 467.93, sys: 30.80, mem: 820468 ko
real: 148.04, user: 467.92, sys: 30.49, mem: 820680 ko
```

With LtacProf, two runs:
```
real: 148.32, user: 469.09, sys: 30.57, mem: 818588 ko
real: 148.38, user: 469.71, sys: 30.56, mem: 816720 ko
```

Overall overhead on building Coq: about 0.24%

Differences in the slowest files:
```
After    | File Name                                | Before   || Change
---------------------------------------------------------------------------
7m07.32s | Total                                    | 7m05.16s || +0m02.15s
---------------------------------------------------------------------------
0m44.90s | Numbers/Rational/BigQ/QMake              | 0m44.11s || +0m00.78s
0m15.94s | plugins/setoid_ring/Ncring_polynom       | 0m15.72s || +0m00.21s
0m14.04s | Numbers/Cyclic/DoubleCyclic/DoubleCyclic | 0m14.05s || -0m00.01s
0m10.65s | Numbers/Cyclic/DoubleCyclic/DoubleSqrt   | 0m10.45s || +0m00.20s
0m09.57s | FSets/FMapAVL                            | 0m09.53s || +0m00.04s
0m09.51s | MSets/MSetRBT                            | 0m09.45s || +0m00.06s
0m07.00s | Numbers/Cyclic/DoubleCyclic/DoubleDiv    | 0m07.05s || -0m00.04s
0m06.88s | Numbers/Cyclic/Int31/Cyclic31            | 0m06.94s || -0m00.06s
0m05.82s | plugins/setoid_ring/Field_theory         | 0m05.87s || -0m00.04s
0m05.74s | FSets/FMapFullAVL                        | 0m05.71s || +0m00.03s
0m05.37s | Reals/Ratan                              | 0m05.42s || -0m00.04s
0m05.36s | plugins/setoid_ring/Ring_polynom         | 0m05.37s || -0m00.00s
0m05.09s | plugins/micromega/EnvRing                | 0m04.96s || +0m00.12s
```
---
 ltacprof/profile_ltac.ml | 45 +++++++++++++++++++++------------------------
 1 file changed, 21 insertions(+), 24 deletions(-)

diff --git a/ltacprof/profile_ltac.ml b/ltacprof/profile_ltac.ml
index 889ae77b8f..71b96614ce 100644
--- a/ltacprof/profile_ltac.ml
+++ b/ltacprof/profile_ltac.ml
@@ -107,22 +107,17 @@ let string_of_call ck =
   let s = try String.sub s 0 (CString.string_index_from s 0 "(*") with Not_found -> s in
   CString.strip s
 
-let exit_tactic option_start_time_add_total c =
-  (match option_start_time_add_total with
-    | Some (start_time, add_total) -> begin
-      try
-        let node :: stack' = !stack in
-        let parent = List.hd stack' in
-        stack := stack';
-        if add_total then Hashtbl.remove on_stack (string_of_call c);
-        let diff = time() -. start_time in
-        parent.entry.local <- parent.entry.local -. diff;
-        add_entry node.entry add_total {total = diff; local = diff; ncalls = 1; max_total = diff};
-      with Failure("hd") -> (* oops, our stack is invalid *)
-	encounter_multi_success_backtracking()
-    end
-    | None -> ()
-  )
+let exit_tactic start_time add_total c =
+  try
+    let node :: stack' = !stack in
+    let parent = List.hd stack' in
+    stack := stack';
+    if add_total then Hashtbl.remove on_stack (string_of_call c);
+    let diff = time() -. start_time in
+    parent.entry.local <- parent.entry.local -. diff;
+    add_entry node.entry add_total {total = diff; local = diff; ncalls = 1; max_total = diff};
+  with Failure("hd") -> (* oops, our stack is invalid *)
+    encounter_multi_success_backtracking()
 
 let tclFINALLY tac (finally : unit Proofview.tactic) =
   let open Proofview.Notations in
@@ -151,14 +146,16 @@ let do_profile s call_trace tac =
           Some (start_time, add_total)
 	)
       | [] -> None
-  else None)) >>= fun option_start_time_add_total ->
-  tclFINALLY
-    tac
-    (Proofview.tclLIFT (Proofview.NonLogical.make (fun () ->
-      (match call_trace with
-      | (_, c) :: _ ->
-        exit_tactic option_start_time_add_total c
-      | [] -> ()))))
+  else None)) >>= function
+  | Some (start_time, add_total) ->
+    tclFINALLY
+      tac
+      (Proofview.tclLIFT (Proofview.NonLogical.make (fun () ->
+	(match call_trace with
+	| (_, c) :: _ ->
+          exit_tactic start_time add_total c
+	| [] -> ()))))
+  | None -> tac
 
 
 
-- 
cgit v1.2.3