Getting rid of Exninfo hacks.

Instead of modifying exceptions to wear additional information, we instead use
a dedicated type now. All exception-using functions were modified to support
this new type, in particular Future's fix_exn-s and the tactic monad.

To solve the problem of enriching exceptions at raise time and recover this
data in the try-with handler, we use a global datastructure recording the
given piece of data imperatively that we retrieve in the try-with handler.
We ensure that such instrumented try-with destroy the data so that there
may not be confusion with another exception. To further harden the correction
of this structure, we also check for pointer equality with the last raised
exception.

The global data structure is not thread-safe for now, which is incorrect as
the STM uses threads and enriched exceptions. Yet, we splitted the patch in
two parts, so that we do not introduce dependencies to the Thread library
immediatly. This will allow to revert only the second patch if ever we
switch to OCaml-coded lightweight threads.

5 files changed, 8 insertions, 7 deletions

diff --git a/library/declaremods.ml b/library/declaremods.ml
index 30cac7771..33d37ef62 100644
--- a/library/declaremods.ml
+++ b/library/declaremods.ml
@@ -796,7 +796,7 @@ let protect_summaries f =
     (* Something wrong: undo the whole process *)
     let reraise = Errors.push reraise in
     let () = Summary.unfreeze_summaries fs in
-    raise reraise
+    iraise reraise
 
 let start_module interp export id args res =
   protect_summaries (RawModOps.start_module interp export id args res)
diff --git a/library/impargs.ml b/library/impargs.ml
index d88d6f106..1a3b88405 100644
--- a/library/impargs.ml
+++ b/library/impargs.ml
@@ -77,7 +77,7 @@ let with_implicits flags f x =
   with reraise ->
     let reraise = Errors.push reraise in
     let () = implicit_args := oflags in
-    raise reraise
+    iraise reraise
 
 let set_maximality imps b =
   (* Force maximal insertion on ending implicits (compatibility) *)
diff --git a/library/library.ml b/library/library.ml
index 4fea6b836..343588652 100644
--- a/library/library.ml
+++ b/library/library.ml
@@ -731,7 +731,7 @@ let save_library_to ?todo dir f otab =
     let () = msg_warning (str ("Removed file "^f')) in
     let () = close_out ch in
     let () = Sys.remove f' in
-    raise reraise
+    iraise reraise
 
 let save_library_raw f lib univs proofs =
   let (f',ch) = raw_extern_library (f^"o") in
diff --git a/library/states.ml b/library/states.ml
index 031222c7d..200b14517 100644
--- a/library/states.ml
+++ b/library/states.ml
@@ -6,6 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
+open Util
 open System
 
 type state = Lib.frozen * Summary.frozen
@@ -38,6 +39,6 @@ let with_state_protection f x =
     let a = f x in unfreeze st; a
   with reraise ->
     let reraise = Errors.push reraise in
-    (unfreeze st; raise reraise)
+    (unfreeze st; iraise reraise)
 
 let with_state_protection_on_exception = Future.transactify
diff --git a/library/summary.ml b/library/summary.ml
index 96b9d0691..7a0064a1f 100644
--- a/library/summary.ml
+++ b/library/summary.ml
@@ -105,8 +105,8 @@ let unfreeze_summaries fs =
     with e when Errors.noncritical e ->
       let e = Errors.push e in
       Printf.eprintf "Error unfrezing summay %s\n%s\n%!"
-        (name_of_summary id) (Pp.string_of_ppcmds (Errors.print e));
-      raise e
+        (name_of_summary id) (Pp.string_of_ppcmds (Errors.iprint e));
+      iraise e
   in
   (** We rely on the order of the frozen list, and the order of folding *)
   ignore (Int.Map.fold_left fold !summaries fs.summaries)
@@ -147,7 +147,7 @@ let unfreeze_summary datas =
       with e ->
         let e = Errors.push e in
         prerr_endline ("Exception unfreezing " ^ name);
-        raise e)
+        iraise e)
   datas
 
 (** All-in-one reference declaration + registration *)