From 20f55b720be8018cdf9690d60e4ed05d9c8ad5c3 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Thu, 25 Jun 2020 20:08:04 +0200
Subject: [exn] Remove some uses of print

Exceptions should not printed except for the top-level.

There is the weird anomaly-absorbing code in `Reductionops`, I wonder
how frequent that case is, but as the exception is absorbed printing
there could have a real impact.
---
 pretyping/reductionops.ml | 13 +++++++++----
 tactics/class_tactics.ml  |  2 +-
 vernac/ppvernac.ml        | 12 +++++-------
 3 files changed, 15 insertions(+), 12 deletions(-)

diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml
index 6f02d76f3a..cb6e8f086e 100644
--- a/pretyping/reductionops.ml
+++ b/pretyping/reductionops.ml
@@ -1097,12 +1097,17 @@ let pb_equal = function
   | Reduction.CUMUL -> Reduction.CONV
   | Reduction.CONV -> Reduction.CONV
 
+exception AnomalyInConversion of exn
+
+let _ = CErrors.register_handler (function
+    | AnomalyInConversion e ->
+      Some Pp.(str "Conversion test raised an anomaly:" ++
+               spc () ++ CErrors.print e)
+    | _ -> None)
+
 let report_anomaly (e, info) =
   let e =
-    if is_anomaly e then
-      let msg = Pp.(str "Conversion test raised an anomaly:" ++
-                    spc () ++ CErrors.print e) in
-      UserError (None, msg)
+    if is_anomaly e then AnomalyInConversion e
     else e
   in
   Exninfo.iraise (e, info)
diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml
index 82ce2234e3..63cafbf76d 100644
--- a/tactics/class_tactics.ml
+++ b/tactics/class_tactics.ml
@@ -236,7 +236,7 @@ let with_prods nprods h f =
             f gl (h, diff)
       with e when CErrors.noncritical e ->
         let e, info = Exninfo.capture e in
-        Tacticals.New.tclZEROMSG ~info (CErrors.print e) end
+        Proofview.tclZERO ~info e end
   else Proofview.Goal.enter
          begin fun gl ->
          if Int.equal nprods 0 then f gl (h, None)
diff --git a/vernac/ppvernac.ml b/vernac/ppvernac.ml
index e0974ac027..b93c920654 100644
--- a/vernac/ppvernac.ml
+++ b/vernac/ppvernac.ml
@@ -1331,10 +1331,8 @@ let pr_vernac_attributes =
   | flags ->  str "#[" ++ pr_vernac_flags flags ++ str "]" ++ cut ()
 
 let pr_vernac ({v = {control; attrs; expr}} as v) =
-  try
-    tag_vernac v
-      (pr_vernac_control control ++
-       pr_vernac_attributes attrs ++
-       pr_vernac_expr expr ++
-       sep_end expr)
-  with e -> CErrors.print e
+  tag_vernac v
+    (pr_vernac_control control ++
+     pr_vernac_attributes attrs ++
+     pr_vernac_expr expr ++
+     sep_end expr)
-- 
cgit v1.2.3


From 619533e81b7396ff9384d603e9d5f431a955578e Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Fri, 26 Jun 2020 14:58:32 +0200
Subject: [reductionops] Comment about absorption of anomalies.

Co-authored-by: <Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>
---
 pretyping/reductionops.ml | 8 ++++++++
 1 file changed, 8 insertions(+)

diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml
index cb6e8f086e..2454f24f25 100644
--- a/pretyping/reductionops.ml
+++ b/pretyping/reductionops.ml
@@ -1097,6 +1097,14 @@ let pb_equal = function
   | Reduction.CUMUL -> Reduction.CONV
   | Reduction.CONV -> Reduction.CONV
 
+(* NOTE: We absorb anomalies happening in the conversion tactic, which
+   is a bit ugly. This is mostly due to efficiency both in tactics and
+   in the conversion machinery itself. It is not uncommon for a tactic
+   to send some ill-typed term to the engine.
+
+   We would usually say that a tactic that converts ill-typed terms is
+   buggy, but fixing the tactic could have a very large runtime cost
+   *)
 exception AnomalyInConversion of exn
 
 let _ = CErrors.register_handler (function
-- 
cgit v1.2.3


From d2ca1efe969ece40254ba19281964c7f391f3f99 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Sat, 27 Jun 2020 16:26:17 +0200
Subject: [error handling] Anomaly in Conversion is a "precatchable_exception"

This is just a fixup, likely all the places that are matching on
`UserErr` directly are just buggy.
---
 pretyping/pretype_errors.ml | 1 +
 pretyping/pretyping.mllib   | 2 +-
 pretyping/reductionops.mli  | 2 ++
 3 files changed, 4 insertions(+), 1 deletion(-)

diff --git a/pretyping/pretype_errors.ml b/pretyping/pretype_errors.ml
index 414663c826..207ffc7b86 100644
--- a/pretyping/pretype_errors.ml
+++ b/pretyping/pretype_errors.ml
@@ -66,6 +66,7 @@ exception PretypeError of env * Evd.evar_map * pretype_error
 
 let precatchable_exception = function
   | CErrors.UserError _ | TypeError _ | PretypeError _
+  | Reductionops.AnomalyInConversion _
   | Nametab.GlobalizationError _ -> true
   | _ -> false
 
diff --git a/pretyping/pretyping.mllib b/pretyping/pretyping.mllib
index 07154d4e03..c31ecc135c 100644
--- a/pretyping/pretyping.mllib
+++ b/pretyping/pretyping.mllib
@@ -1,8 +1,8 @@
 Geninterp
 Locus
 Locusops
-Pretype_errors
 Reductionops
+Pretype_errors
 Inductiveops
 Arguments_renaming
 Retyping
diff --git a/pretyping/reductionops.mli b/pretyping/reductionops.mli
index b316b3c213..f8c9af7cad 100644
--- a/pretyping/reductionops.mli
+++ b/pretyping/reductionops.mli
@@ -293,3 +293,5 @@ val whd_betaiota_deltazeta_for_iota_state :
 (** {6 Meta-related reduction functions } *)
 val meta_instance : env -> evar_map -> constr freelisted -> constr
 val nf_meta       : env -> evar_map -> constr -> constr
+
+exception AnomalyInConversion of exn
-- 
cgit v1.2.3