Merge PR rocq-prover#21252: Ltac2: provide user API for printing errors

Reviewed-by: thomas-lamiaux
Ack-by: JasonGross
Co-authored-by: thomas-lamiaux <thomas-lamiaux@users.noreply.github.com>

Author: coqbot-app[bot]

doc/changelog/06-Ltac2-language/21252-pr-tac2fail-Added.rst

@@ -0,0 +1,4 @@
+- **Added:**
+  APIs `Control.print_err` and `Control.print_exn` which may be used to customize printing of Ltac2 errors
+  (`#21252 <https://github.com/rocq-prover/rocq/pull/21252>`_,
+  by Gaëtan Gilbert).

plugins/ltac2/tac2core.ml

@@ -992,6 +992,8 @@ let () = define "current_exninfo" (unit @-> tac exninfo) @@ fun () ->
 
 let () = define "message_of_exninfo" (exninfo @-> ret pp) CErrors.print_extra
 
+let () = define "print_err" (err @-> ret pp) @@ fun (e,_) -> CErrors.print e
+
 (** Control *)
 
 (** exn -> 'a *)

plugins/ltac2/tac2entries.ml

@@ -1333,13 +1333,45 @@ let pr_frame = function
     str "Extn " ++ str (Tac2dyn.Arg.repr tag) ++ str ":" ++ spc () ++
     obj.Tac2env.ml_print env sigma arg
 
-let () = register_handler begin function
-| Tac2interp.LtacError (kn, args) ->
+let print_raw_error kn args =
   let t_exn = KerName.make Tac2env.rocq_prefix (Id.of_string "exn") in
   let v = Tac2ffi.of_open (kn, args) in
   let t = GTypRef (Other t_exn, []) in
   let c = Tac2print.pr_valexpr (Global.env ()) Evd.empty v t in
-  Some (hov 0 (str "Uncaught Ltac2 exception:" ++ spc () ++ hov 0 c))
+  hov 0 (str "Uncaught Ltac2 exception:" ++ spc () ++ hov 0 c)
+
+let print_error kn args =
+  let env = Global.env() in
+  let sigma = Evd.from_env env in
+  let user_print = KerName.make Tac2quote.Refs.control_prefix (Id.of_string "print_exn") in
+  let user_print = Tac2interp.eval_global user_print in
+  let user_print = Tac2ffi.(to_fun1 of_exn (to_option to_pp)) user_print in
+  let user_print () =
+    let res, _, _, _, _ =
+    Proofview.apply ~name:(Id.of_string_soft "ltac2 error printing") ~poly:PolyFlags.default
+      env
+      (user_print (Tac2interp.LtacError (kn, args), Exninfo.null))
+      (snd @@ Proofview.init sigma [])
+    in
+    res
+  in
+  match user_print() with
+  | Some msg -> msg
+  | None -> print_raw_error kn args
+  | exception e when CErrors.noncritical e ->
+    let e = Exninfo.capture e in
+    let ppe = match e with
+      | Tac2interp.LtacError (kn', args'), _info ->
+        (* don't use iprint: high risk of looping *)
+        (* XXX print the info? currently CErrors.print_extra is not exposed *)
+        print_raw_error kn' args'
+      | _ -> CErrors.iprint e
+    in
+    print_raw_error kn args ++ fnl() ++
+    hov 2 (str "Custom Ltac2 printer failed:" ++ spc() ++ ppe)
+
+let () = register_handler begin function
+| Tac2interp.LtacError (kn, args) -> Some (print_error kn args)
 | _ -> None
 end
 

plugins/ltac2/tac2quote.mli

@@ -49,6 +49,8 @@ module Refs : sig
 
   val t_module : type_constant
 
+  (** Modules *)
+  val control_prefix : ModPath.t
 end
 
 val constructor : ?loc:Loc.t -> ltac_constructor -> raw_tacexpr list -> raw_tacexpr

test-suite/output/ltac2_print_exn.out

@@ -0,0 +1,17 @@
+File "./output/ltac2_print_exn.v", line 11, characters 0-23:
+The command has indeed failed with message:
+hello
+Backtrace:
+Call foo
+Prim <rocq-runtime.plugins.ltac2:zero>
+
+File "./output/ltac2_print_exn.v", line 24, characters 0-23:
+The command has indeed failed with message:
+Uncaught Ltac2 exception: WithTerm constr:(?X1)
+File "./output/ltac2_print_exn.v", line 33, characters 0-23:
+The command has indeed failed with message:
+test ?X1
+File "./output/ltac2_print_exn.v", line 38, characters 0-23:
+The command has indeed failed with message:
+Uncaught Ltac2 exception: Tactic_failure (Some message:(hello))
+Custom Ltac2 printer failed: Uncaught Ltac2 exception: Assertion_failure

test-suite/output/ltac2_print_exn.v

@@ -0,0 +1,38 @@
+Require Import Ltac2.Ltac2.
+Import Printf.
+
+(** basic test, we also check that the backtrace isn't forgotten when
+    using the custom printer *)
+
+Set Ltac2 Backtrace.
+
+Ltac2 foo () := Control.zero (Tactic_failure (Some (Message.of_string "hello"))).
+
+Fail Ltac2 Eval foo ().
+
+Unset Ltac2 Backtrace.
+
+(** Test printing constr even though we have a bad evar map *)
+
+Ltac2 Type exn ::= [ WithTerm (constr) ].
+
+Ltac2 bar () :=
+  let c := open_constr:(_ :> nat) in
+  Control.zero (WithTerm c).
+
+(* default printer doesn't have the evar map but doesn't fail *)
+Fail Ltac2 Eval bar ().
+
+Ltac2 Set Control.print_exn := fun e =>
+  match e with
+  |  WithTerm c => Some (fprintf "test %t" c)
+  | _ => None
+  end.
+
+(* custom printer also doesn't have the evar map but doesn't fail *)
+Fail Ltac2 Eval bar ().
+
+(** Test custom printer producing an error *)
+Ltac2 Set Control.print_exn := fun _ => Control.throw Assertion_failure.
+
+Fail Ltac2 Eval foo ().

theories/Ltac2/Control.v

@@ -224,3 +224,31 @@ Ltac2 @ external timeout : int -> (unit -> 'a) -> 'a :=
 (** [timeoutf t thunk] calls [thunk ()] with a timeout of [t] seconds. *)
 Ltac2 @ external timeoutf : float -> (unit -> 'a) -> 'a :=
   "rocq-runtime.plugins.ltac2" "timeoutf".
+
+(** Error printing *)
+
+(** Print internal errors. *)
+Ltac2 @external print_err : err -> message
+  := "rocq-runtime.plugins.ltac2" "print_err".
+
+(** Print exceptions as errors. Used by the runtime when printing uncaught errors.
+    Extensible by mutation, see uses below.
+
+    IMPORTANT: when called for printing uncaught errors, it is run in an empty state
+    (no goals, empty evar map).
+
+    Also note that the "Internal" branch is not used when printing
+    uncaught errors as Internal exceptions are not considered as Ltac2
+    errors. *)
+Ltac2 mutable print_exn : exn -> message option := fun e =>
+  match e with
+  | Internal e => Some (print_err e)
+  | _ => None
+  end.
+
+#[global]
+Ltac2 Set print_exn as print_other := fun e =>
+  match e with
+  | Tactic_failure (Some msg) => Some msg
+  | _ => print_other e
+  end.