From ade57e8bd792a9575d0c3dc890361d944adfe42e Mon Sep 17 00:00:00 2001
From: Davide Fissore <fisso9900@gmail.com>
Date: Thu, 27 Jun 2024 16:09:40 +0200
Subject: [PATCH 1/2] More time for benching

elpitime (if active) also prints the time of get_and-compile
run_static_check try/catch error so that elpitime message can be displayed.
the elpitime message will tell if the execution was successfull or not
---
 src/coq_elpi_vernacular.ml | 31 +++++++++++++++++++------------
 1 file changed, 19 insertions(+), 12 deletions(-)

diff --git a/src/coq_elpi_vernacular.ml b/src/coq_elpi_vernacular.ml
index 6a03e78f3..a74c1a6d8 100644
--- a/src/coq_elpi_vernacular.ml
+++ b/src/coq_elpi_vernacular.ml
@@ -176,7 +176,8 @@ let compile src =
     compile_code src
 
 let get_and_compile ?even_if_empty name : (EC.program * bool) option =
-  P.code ?even_if_empty name |> Option.map (fun src ->
+  let t = Unix.gettimeofday () in
+  let res = P.code ?even_if_empty name |> Option.map (fun src ->
     let prog = compile src in
     let new_hash = Code.hash src in
     let old_hash = try SLMap.find name !programs_tip with Not_found -> 0 in
@@ -187,7 +188,9 @@ let get_and_compile ?even_if_empty name : (EC.program * bool) option =
       | Command { raw_args } -> raw_args
       | Program { raw_args } -> raw_args
       | Tactic -> true in
-    (prog, raw_args))
+      (prog, raw_args)) in
+    Coq_elpi_utils.elpitime (fun _ -> Pp.(str(Printf.sprintf "Elpi: get_and_compile %1.4f" (Unix.gettimeofday () -. t))));
+    res
 
 let run_static_check query =
   let checker = 
@@ -218,16 +221,20 @@ let run ~static_check program query =
     CErrors.user_err Pp.(str"Unknown trace options: " ++ prlist_with_sep spc str leftovers);
   let exe = EC.optimize query in
   let t4 = Unix.gettimeofday () in
-  let rc = API.Execute.once ~max_steps:!max_steps exe in
-  let t5 = Unix.gettimeofday () in
-  Coq_elpi_utils.debug Pp.(fun () ->
-      str @@ Printf.sprintf
-        "Elpi: query-compilation:%1.4f static-check:%1.4f optimization:%1.4f runtime:%1.4f\n"
-        (t2 -. t1) (t3 -. t2) (t4 -. t3) (t5 -. t4));
-  Coq_elpi_utils.elpitime Pp.(fun () -> str @@ Printf.sprintf
-        "Elpi: query-compilation:%1.4f static-check:%1.4f optimization:%1.4f runtime:%1.4f\n"
-        (t2 -. t1) (t3 -. t2) (t4 -. t3) (t5 -. t4));
-  rc
+  let print_debug with_error = 
+    let t5 = Unix.gettimeofday () in
+    let txt = Printf.sprintf "Elpi: query-compilation:%1.4f static-check:%1.4f optimization:%1.4f runtime:%1.4f %s\n"
+        (t2 -. t1) (t3 -. t2) (t4 -. t3) (t5 -. t4) (if with_error then "(with error)" else "(with success)") in
+    Coq_elpi_utils.debug Pp.(fun () -> str txt);
+    Coq_elpi_utils.elpitime Pp.(fun () -> str txt)
+  in
+  try
+    let rc = API.Execute.once ~max_steps:!max_steps exe in
+    print_debug false;
+    rc
+  with e ->
+    print_debug true;
+    raise e
 ;;
 
 let elpi_fails program_name =

From feb92fcd61af80190fbe5ea1bd56de34edbdebe7 Mon Sep 17 00:00:00 2001
From: Enrico Tassi <Enrico.Tassi@inria.fr>
Date: Fri, 28 Jun 2024 11:34:17 +0200
Subject: [PATCH 2/2] Update src/coq_elpi_vernacular.ml

---
 src/coq_elpi_vernacular.ml | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/src/coq_elpi_vernacular.ml b/src/coq_elpi_vernacular.ml
index a74c1a6d8..cd9022ed3 100644
--- a/src/coq_elpi_vernacular.ml
+++ b/src/coq_elpi_vernacular.ml
@@ -233,8 +233,9 @@ let run ~static_check program query =
     print_debug false;
     rc
   with e ->
+    let e = Exninfo.capture e in
     print_debug true;
-    raise e
+    Exninfo.iraise e
 ;;
 
 let elpi_fails program_name =