[quickfix] warnings and errors can carry a qf in the vscode sense

ide/coqide/coqOps.ml

@@ -643,28 +643,28 @@ object(self)
           self#attach_tooltip ~loc sentence
             (Printf.sprintf "%s %s %s" filepath ident ty)
       | GlobRef (_, _, _, _, _), None -> msg_wo_sent "GlobRef"
-      | Message(Error, loc, msg), Some (id,sentence) ->
+      | Message(Error, loc, _, msg), Some (id,sentence) ->
           log_pp ?id Pp.(str "ErrorMsg " ++ msg);
           remove_flag sentence `PROCESSING;
           let rmsg = Pp.string_of_ppcmds msg in
           add_flag sentence (`ERROR (loc, rmsg));
           self#mark_as_needed sentence;
           self#attach_tooltip ?loc sentence rmsg;
           self#apply_tag_in_sentence ?loc Tags.Script.error sentence
-      | Message(Warning, loc, message), Some (id,sentence) ->
+      | Message(Warning, loc, _, message), Some (id,sentence) ->
           log_pp ?id Pp.(str "WarningMsg " ++ message);
           let rmsg = Pp.string_of_ppcmds message in
           add_flag sentence (`WARNING (loc, rmsg));
           self#attach_tooltip ?loc sentence rmsg;
           self#apply_tag_in_sentence ?loc Tags.Script.warning sentence;
           (messages#route msg.route)#push Warning message
-      | Message(lvl, loc, message), Some (id,sentence) ->
+      | Message(lvl, loc, _, message), Some (id,sentence) ->
           log_pp ?id Pp.(str "Msg " ++ message);
           (messages#route msg.route)#push lvl message
       (* We do nothing here as for BZ#5583 *)
-      | Message(Error, loc, msg), None ->
+      | Message(Error, loc, _, msg), None ->
           log_pp Pp.(str "Error Msg without a sentence" ++ msg)
-      | Message(lvl, loc, message), None ->
+      | Message(lvl, loc, _, message), None ->
           log_pp Pp.(str "Msg without a sentence " ++ message);
           (messages#route msg.route)#push lvl message
       | InProgress n, _ ->

ide/coqide/idetop.ml

@@ -76,7 +76,7 @@ let is_known_option cmd = match cmd with
   | _ -> false
 
 let ide_cmd_warns ~id { CAst.loc; v } =
-  let warn msg = Feedback.(feedback ~id (Message (Warning, loc, strbrk msg))) in
+  let warn msg = Feedback.(feedback ~id (Message (Warning, loc, [], strbrk msg))) in
   if is_known_option v.expr then
     warn "Set this option from the IDE menu instead";
   if is_navigation_vernac v.expr || is_undo v.expr then

ide/coqide/protocol/xmlprotocol.ml

@@ -1048,7 +1048,7 @@ let of_message lvl loc msg =
 
 let to_message xml = match xml with
   | Xml_datatype.Element ("message", [], [lvl; xloc; content]) ->
-      Message(to_message_level lvl, to_option to_loc xloc, to_pp content)
+      Message(to_message_level lvl, to_option to_loc xloc, [], to_pp content)
   | x -> raise (Marshal_error("message",x))
 
 let to_feedback_content = do_match "feedback_content" (fun s a -> match s,a with
@@ -1108,7 +1108,7 @@ let of_feedback_content = function
       constructor "feedback_content" "fileloaded" [
         of_string dirpath;
         of_string filename ]
-  | Message (l,loc,m) -> constructor "feedback_content" "message" [ of_message l loc m ]
+  | Message (l,loc,_,m) -> constructor "feedback_content" "message" [ of_message l loc m ]
 
 let of_edit_or_state_id id = ["object","state"], of_stateid id
 

lib/cErrors.ml

@@ -128,9 +128,17 @@ let print_gen ~anomaly (e, info) =
     str "<in exception printer>:" ++ spc() ++ print_anomaly anomaly exn ++ print_extra info ++ fnl() ++
     str "<original exception>:" ++ spc() ++ print_anomaly false e ++ extra_msg
 
+let print_quickfix = function
+  | [] -> mt ()
+  | qf -> fnl () ++ Quickfix.print qf
+
 (** The standard exception printer *)
 let iprint (e, info) =
-  print_gen ~anomaly:true (e,info)
+  print_gen ~anomaly:true (e,info) ++
+  if !Flags.test_mode then
+    Result.fold ~ok:print_quickfix ~error:(print_gen ~anomaly:true) (Quickfix.from_exception e)
+  else
+    mt ()
 
 let print e =
   iprint (e, Exninfo.info e)

lib/cWarnings.ml

@@ -72,7 +72,7 @@ let get_status ~name = match get_warning name with
 
 type _ tag = ..
 
-type w = W : 'a tag * 'a -> w
+type w = W : 'a tag * Quickfix.t list * 'a -> w
 exception WarnError of w
 
 module DMap = PolyMap.Make (struct type nonrec 'a tag = 'a tag = .. end)
@@ -100,20 +100,24 @@ let create_msg warning () =
   let v = { Msg.tag = DMap.make(); warning; } in
   v
 
-let print (W (tag, w)) =
+let print (W (tag,_, w)) =
   let pp = try PrintMap.find tag !printers with Not_found -> assert false in
   pp w
 
 let () = CErrors.register_handler (function
     | WarnError w -> Some (print w)
     | _ -> None)
 
-let warn { Msg.tag; warning } ?loc v =
+let () = Quickfix.register (function
+| WarnError (W(_,qf,_)) -> qf
+| _ -> [])
+
+let warn { Msg.tag; warning } ?loc ?(quickfix=[]) v =
   let tag = DMap.tag_of_onetag tag in
   match warning_status warning with
   | Disabled -> ()
-  | AsError -> Loc.raise ?loc (WarnError (W (tag, v)))
-  | Enabled -> Feedback.msg_warning ?loc (print (W (tag, v)))
+  | AsError -> Loc.raise ?loc (WarnError (W (tag,quickfix,v)))
+  | Enabled -> Feedback.msg_warning ?loc ~quickfix (print (W (tag,quickfix,v)))
 
 (** Flag handling *)
 
@@ -375,13 +379,17 @@ let create_hybrid ?from ?default ~name () =
 let create_in w pp =
   let msg = create_msg w () in
   let () = register_printer msg pp in
-  fun ?loc x -> warn ?loc msg x
+  fun ?loc ?quickfix x -> warn ?loc ?quickfix msg x
 
-let create ~name ?category ?default pp =
+let create_with_quickfix ~name ?category ?default pp =
   let from = Option.map (fun x -> [x]) category in
   let w = create_warning ?from ?default ~name () in
   create_in w pp
 
+let create ~name ?category ?default pp =
+  let f = create_with_quickfix ~name ?category ?default pp in
+  fun ?loc x -> f ?quickfix:None ?loc x
+
 let warn_unknown_warnings = create ~name:"unknown-warning" Pp.(fun flags ->
     str "Could not enable unknown " ++
     str (CString.plural (List.length flags) "warning") ++ spc() ++

lib/cWarnings.mli

@@ -23,7 +23,7 @@ type warning
 type 'a msg
 (** A [msg] belongs to a [warning]. *)
 
-val warn : 'a msg -> ?loc:Loc.t -> 'a -> unit
+val warn : 'a msg -> ?loc:Loc.t -> ?quickfix:Quickfix.t list -> 'a -> unit
 (** Emit a message in some warning. *)
 
 (** Creation functions
@@ -46,7 +46,7 @@ val create_hybrid : ?from:category list -> ?default:status -> name:string -> uni
 val create_msg : warning -> unit -> 'a msg
 (** A message with data ['a] in the given warning. *)
 
-val create_in : warning -> ('a -> Pp.t) -> ?loc:Loc.t -> 'a -> unit
+val create_in : warning -> ('a -> Pp.t) -> ?loc:Loc.t -> ?quickfix:Quickfix.t list -> 'a -> unit
 (** Create a msg with registered printer. *)
 
 val register_printer : 'a msg -> ('a -> Pp.t) -> unit
@@ -56,6 +56,10 @@ val create : name:string -> ?category:category -> ?default:status ->
   ('a -> Pp.t) -> ?loc:Loc.t -> 'a -> unit
 (** Combined creation function. [name] must be a fresh name. *)
 
+val create_with_quickfix : name:string -> ?category:category -> ?default:status ->
+    ('a -> Pp.t) -> ?loc:Loc.t -> ?quickfix:Quickfix.t list -> 'a -> unit
+  (** Combined creation function. [name] must be a fresh name. *)
+
 (** Misc APIs *)
 
 val get_flags : unit -> string

lib/feedback.ml

@@ -42,7 +42,7 @@ type feedback_content =
   (* Extra metadata *)
   | Custom of Loc.t option * string * xml
   (* Generic messages *)
-  | Message of level * Loc.t option * Pp.t
+  | Message of level * Loc.t option * Quickfix.t list * Pp.t
 
 type feedback = {
   doc_id   : doc_id;            (* The document being concerned *)
@@ -83,19 +83,19 @@ let feedback ?did ?id ?route what =
   if !warn_no_listeners && Hashtbl.length feeders = 0 then begin
     Format.eprintf "Warning, feedback message received but no listener to handle it!@\n%!";
     match m.contents with
-    | Message (lvl,_,msg) ->
+    | Message (lvl,_,_,msg) ->
       Format.eprintf "%a%a" pp_lvl lvl Pp.pp_with msg
     | _ -> ()
   end ;
   Hashtbl.iter (fun _ f -> f m) feeders
 
 (* Logging messages *)
-let feedback_logger ?loc lvl msg =
-  feedback ~route:!feedback_route ~id:!span_id (Message (lvl, loc, msg))
+let feedback_logger ?loc ?(quickfix=[]) lvl msg =
+  feedback ~route:!feedback_route ~id:!span_id (Message (lvl, loc, quickfix, msg))
 
 let msg_info    ?loc x = feedback_logger ?loc Info x
 let msg_notice  ?loc x = feedback_logger ?loc Notice x
-let msg_warning ?loc x = feedback_logger ?loc Warning x
+let msg_warning ?loc ?quickfix x = feedback_logger ?loc ?quickfix Warning x
 (* let msg_error   ?loc x = feedback_logger ?loc Error x *)
 let msg_debug   ?loc x = feedback_logger ?loc Debug x
 
@@ -123,6 +123,6 @@ let console_feedback_listener fmt =
   | FileDependency (_,_) -> ()
   | FileLoaded (_,_) -> ()
   | Custom (_,_,_) -> ()
-  | Message (lvl,loc,msg) ->
+  | Message (lvl,loc,_,msg) ->
     fprintf fmt "@[%a@]%a@[%a@]\n%!" pp_loc loc pp_lvl lvl Pp.pp_with msg
   in checker_feed

lib/feedback.mli

@@ -45,7 +45,7 @@ type feedback_content =
   (* Extra metadata *)
   | Custom of Loc.t option * string * xml
   (* Generic messages *)
-  | Message of level * Loc.t option * Pp.t
+  | Message of level * Loc.t option * Quickfix.t list * Pp.t
 
 type feedback = {
   doc_id   : doc_id;            (* The document being concerned *)
@@ -86,9 +86,9 @@ val msg_info : ?loc:Loc.t -> Pp.t -> unit
 val msg_notice : ?loc:Loc.t -> Pp.t -> unit
 (** Message that should be displayed, such as [Print Foo] or [Show Bar]. *)
 
-val msg_warning : ?loc:Loc.t -> Pp.t -> unit
+val msg_warning : ?loc:Loc.t -> ?quickfix:Quickfix.t list -> Pp.t -> unit
 (** Message indicating that something went wrong, but without serious
-    consequences. *)
+    consequences. A list of quick fixes, in the VSCode sense, can be provided *)
 
 val msg_debug : ?loc:Loc.t -> Pp.t -> unit
 (** For debugging purposes *)

lib/flags.ml

@@ -85,3 +85,5 @@ let profile_ltac_cutoff = ref 2.0
 (* Default output directory *)
 
 let output_directory = ref None
+
+let test_mode = ref false

lib/flags.mli

@@ -100,3 +100,8 @@ val profile_ltac_cutoff : float ref
 
 (** Default output directory *)
 val output_directory : CUnix.physical_path option ref
+
+
+(** Flag set when the test-suite is called. Its only effect to display
+    verbose information for [Fail] *)
+val test_mode : bool ref

lib/quickfix.ml

@@ -0,0 +1,41 @@
+(************************************************************************)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *         Copyright INRIA, CNRS and contributors             *)
+(* <O___,, * (see version control and CREDITS file for authors & dates) *)
+(*   \VV/  **************************************************************)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
+(************************************************************************)
+
+(* Quickfix management *)
+
+type t = Loc.t * Pp.t
+let make ~loc txt = loc, txt
+let pp (_,x) = x
+let loc (l,_) = l
+
+let handle_stack = ref []
+
+let register h = handle_stack := h::!handle_stack
+
+let rec accumulate_qf acc stk e =
+  match stk with
+  | [] -> acc
+  | h::stk -> accumulate_qf (h e :: acc) stk e
+
+let from_exception e =
+  try
+    Ok (CList.flatten (accumulate_qf [] !handle_stack e))
+  with exn ->
+    let ei = Exninfo.capture exn in
+    Error ei
+
+let print e =
+  let open Pp in
+  match e with
+  | [] -> mt ()
+  | qf ->
+    let open Pp in
+    let qf = prlist_with_sep cut pp qf in
+    v 0 (prlist_with_sep cut (fun x -> x) [str "Quickfix:"; qf])

lib/quickfix.mli

@@ -0,0 +1,37 @@
+(************************************************************************)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *         Copyright INRIA, CNRS and contributors             *)
+(* <O___,, * (see version control and CREDITS file for authors & dates) *)
+(*   \VV/  **************************************************************)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
+(************************************************************************)
+
+type t
+
+val make : loc:Loc.t -> Pp.t -> t
+
+val pp : t -> Pp.t
+
+val loc : t -> Loc.t
+
+(** [register h] registers [h] as a quickfix generator.
+    When an error is generated the toplevel can check if there is
+    quick fix for it.
+
+    Quickfix generators signal that they don't deal with some exception
+    by returning []. Raising any other exception is
+    forbidden.
+
+    Exceptions that are considered anomalies should not be
+    handled by Quickfix generators.
+*)
+
+val register : (exn -> t list) -> unit
+
+(** computes all the quickfixes for a given exception *)
+val from_exception : exn -> (t list, Exninfo.iexn) result
+
+(** Prints all the quickfixes in a vertical box *)
+val print : t list -> Pp.t

stm/asyncTaskQueue.ml

@@ -308,8 +308,8 @@ module Make(T : Task) () = struct
   let pp_pid pp = Pp.(str (Spawned.process_id () ^ " ") ++ pp)
 
   let debug_with_pid = Feedback.(function
-    | { contents = Message(Debug, loc, pp) } as fb ->
-       { fb with contents = Message(Debug,loc, pp_pid pp) }
+    | { contents = Message(Debug, loc, qf, pp) } as fb ->
+       { fb with contents = Message(Debug,loc, qf, pp_pid pp) }
     | x -> x)
 
   let main_loop () =

stm/stm.ml

@@ -88,7 +88,7 @@ let async_proofs_is_master opt =
   !Flags.async_proofs_worker_id = "master"
 
 let execution_error ?loc state_id msg =
-    feedback ~id:state_id (Message (Error, loc, msg))
+    feedback ~id:state_id (Message (Error, loc, [], msg))
 
 module Hooks = struct
 
@@ -1699,9 +1699,10 @@ end = struct (* {{{ *)
       ignore(stm_vernac_interp r_for st { r_what with verbose = true });
       feedback ~id:r_for Processed
     with e when CErrors.noncritical e ->
-      let e = Exninfo.capture e in
-      let msg = iprint e     in
-      feedback ~id:r_for (Message (Error, None, msg))
+      let e,_ as ie = Exninfo.capture e in
+      let msg = iprint ie in
+      let qf = Result.value ~default:[] (Quickfix.from_exception e) in
+      feedback ~id:r_for (Message (Error, None, qf, msg))
 
   let name_of_task { t_what } = string_of_ppcmds (pr_ast t_what)
   let name_of_request { r_what } = string_of_ppcmds (pr_ast r_what)

sysinit/coqargs.ml

@@ -394,7 +394,7 @@ let parse_args ~usage ~init arglist : t * string list =
       { oval with config = {oval.config with native_include_dirs = include_dir :: oval.config.native_include_dirs } }
 
     (* Options with zero arg *)
-    |"-test-mode" -> Synterp.test_mode := true; oval
+    |"-test-mode" -> Flags.test_mode := true; oval
     |"-beautify" -> Flags.beautify := true; Flags.record_comments := true; oval
     |"-config"|"--config" -> set_query oval PrintConfig
 

topbin/coqnative_bin.ml

@@ -260,7 +260,7 @@ let init_load_path ~boot ~vo_path =
 let fb_handler = function
   | Feedback.{ contents; _ } ->
     match contents with
-    | Feedback.Message(_lvl,_loc,msg)->
+    | Feedback.Message(_lvl,_loc,_qf, msg)->
       Format.printf "%s@\n%!" Pp.(string_of_ppcmds msg)
     | _ -> ()