From 7e078b070b3acf6c0b24d66a150b09a7df57b09d Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Tue, 11 Feb 2020 11:33:55 +0100
Subject: [misc] Better preserve backtraces in several modules

Re-raising inside exception handlers must be done with care in order
to preserve backtraces; even if newer OCaml versions do a better job
in automatically spilling `%reraise` in places that matter, there is
no guarantee for that to happen.

I've done a best-effort pass of places that were re-raising
incorrectly, hopefully I got the logic right.

There is the special case of `Nametab.error_global_not_found` which is
raised many times in response to a `Not_found` error; IMHO this error
should be converted to something more specific, however the scope of
that change would be huge as to do easily...
---
 library/nametab.ml  | 16 ++++++++++------
 library/nametab.mli |  2 +-
 2 files changed, 11 insertions(+), 7 deletions(-)

(limited to 'library')

diff --git a/library/nametab.ml b/library/nametab.ml
index d9b4dc9122..a51c281f2b 100644
--- a/library/nametab.ml
+++ b/library/nametab.ml
@@ -43,8 +43,9 @@ end
 
 exception GlobalizationError of qualid
 
-let error_global_not_found qid =
-  Loc.raise ?loc:qid.CAst.loc (GlobalizationError qid)
+let error_global_not_found ~info qid =
+  let info = Option.cata (Loc.add_loc info) info qid.CAst.loc in
+  Exninfo.iraise (GlobalizationError qid, info)
 
 (* The visibility can be registered either
    - for all suffixes not shorter then a given int - when the object
@@ -499,8 +500,9 @@ let global qid =
         user_err ?loc:qid.CAst.loc ~hdr:"global"
           (str "Unexpected reference to a notation: " ++
            pr_qualid qid)
-  with Not_found ->
-    error_global_not_found qid
+  with Not_found as exn ->
+    let _, info = Exninfo.capture exn in
+    error_global_not_found ~info qid
 
 (* Exists functions ********************************************************)
 
@@ -566,8 +568,10 @@ let shortest_qualid_of_universe ?loc kn =
 
 let pr_global_env env ref =
   try pr_qualid (shortest_qualid_of_global env ref)
-  with Not_found as e ->
-    if !Flags.debug then Feedback.msg_debug (Pp.str "pr_global_env not found"); raise e
+  with Not_found as exn ->
+    let exn, info = Exninfo.capture exn in
+    if !Flags.debug then Feedback.msg_debug (Pp.str "pr_global_env not found");
+    Exninfo.iraise (exn, info)
 
 let global_inductive qid =
   let open GlobRef in
diff --git a/library/nametab.mli b/library/nametab.mli
index 00cec35506..8a8b59733c 100644
--- a/library/nametab.mli
+++ b/library/nametab.mli
@@ -91,7 +91,7 @@ end
 exception GlobalizationError of qualid
 
 (** Raises a globalization error *)
-val error_global_not_found : qualid -> 'a
+val error_global_not_found : info:Exninfo.info -> qualid -> 'a
 
 (** {6 Register visibility of things } *)
 
-- 
cgit v1.2.3