Capture Output command modified

coqpp/coqpp_main.ml

@@ -437,6 +437,7 @@ let understand_state = function
   | "declare_program" -> "vtdeclareprogram", ["pm"]
   | "program_interactive" -> "vtopenproofprogram", ["pm"]
   | "opaque_access" -> "vtopaqueaccess", ["opaque_access"]
+  | "consume_captured_output" -> "vtconsumecapturedoutput", ["captured"]
   | s -> fatal ("unsupported state specifier: " ^ s)
 
 let rec pr_named_arguments fmt = function

doc/sphinx/proof-engine/vernacular-commands.rst

@@ -1244,6 +1244,34 @@ Controlling Typing Flags
 
 Typing flags may not be changed while inside sections.
 
+Output testing
+--------------
+
+.. cmd:: Capture Output @sentence
+
+   If :n:`@sentence` succeeds, copies the messages it printed to the
+   "captured output" internal state.
+
+.. cmd:: Assert Captured Output {? ( {*, @captured_output_flag } ) } @string
+
+   .. insertprodn captured_output_flag captured_output_flag
+
+   .. prodn::
+      captured_output_flag ::= no drop
+      | printing width @natural
+
+   Fails if the current captured output is not equal to the given string.
+   Printing width is currently required.
+   Unless `no drop` is specified, the captured output state is cleared.
+
+.. cmd:: Drop Captured Output
+
+   Deletes the contents of the "captured output" internal state.
+
+.. cmd:: Print Captured Output
+
+   Print the current contents of the "captured output" internal state.
+
 .. _internal-registration-commands:
 
 Internal registration commands

doc/tools/docgram/common.edit_mlg

@@ -1584,6 +1584,8 @@ control_flag: [
 | WITH "Fail" sentence
 | REPLACE "Succeed"
 | WITH "Succeed" sentence
+| REPLACE "Capture" "Output"
+| WITH "Capture" "Output" sentence
 ]
 
 vernac_control: [

doc/tools/docgram/fullGrammar

@@ -566,6 +566,8 @@ command: [
 | "Test" setting_name
 | "Remove" IDENT IDENT LIST1 table_value
 | "Remove" IDENT LIST1 table_value
+| "Drop" "Captured" "Output"
+| "Assert" "Captured" "Output" OPT [ "(" LIST0 captured_output_flag SEP "," ")" ] lstring
 | "Reset" "Initial"
 | "Reset" identref
 | "Back"
@@ -831,6 +833,7 @@ control_flag: [
 | "AllocLimit" natural [ "Mw" | "kw" ]
 | "Fail"
 | "Succeed"
+| "Capture" "Output"
 ]
 
 decorated_vernac: [
@@ -1453,6 +1456,7 @@ printable: [
 | "Strategies"
 | "Registered"
 | "Registered" "Schemes"
+| "Captured" "Output"
 ]
 
 debug_univ_name: [
@@ -1567,6 +1571,11 @@ univ_name_list: [
 | "@{" LIST0 name OPT [ ";" LIST0 name ] "}"
 ]
 
+captured_output_flag: [
+| "no" "drop"
+| "printing" "width" natural
+]
+
 syntax: [
 | "Open" "Scope" IDENT
 | "Close" "Scope" IDENT

doc/tools/docgram/orderedGrammar

@@ -795,6 +795,7 @@ command: [
 | "Print" "Strategies"
 | "Print" "Registered"
 | "Print" "Registered" "Schemes"
+| "Print" "Captured" "Output"
 | "Print" OPT "Term" LIST1 [ reference OPT univ_name_list ] SEP ","
 | "Print" "Module" "Type" qualid
 | "Print" "Module" qualid
@@ -810,6 +811,8 @@ command: [
 | "Debug" [ "On" | "Off" ]
 | "Declare" "Reduction" ident ":=" red_expr
 | "Declare" "Custom" "Entry" ident
+| "Drop" "Captured" "Output"
+| "Assert" "Captured" "Output" OPT [ "(" LIST0 captured_output_flag SEP "," ")" ] string
 | "Derive" open_binders "SuchThat" type "As" ident
 | "Derive" open_binders "in" type "as" ident
 | "Extraction" qualid      (* extraction plugin *)
@@ -1041,6 +1044,7 @@ command: [
 | "AllocLimit" natural [ "Mw" | "kw" ] sentence
 | "Fail" sentence
 | "Succeed" sentence
+| "Capture" "Output" sentence
 | "Drop"
 | "Quit"
 | "BackTo" natural
@@ -1101,6 +1105,11 @@ univ_name_list: [
 | "@{" LIST0 name OPT [ ";" LIST0 name ] "}"
 ]
 
+captured_output_flag: [
+| "no" "drop"
+| "printing" "width" natural
+]
+
 enable_notation_flag: [
 | "all"
 | "only" "parsing"

test-suite/output/captured_output.out

@@ -0,0 +1,72 @@
+0
+     : nat
+1
+     : nat
+2
+     : nat
+File "./output/captured_output.v", line 7, characters 21-24:
+Warning: hello [warn-reference,user-warn,default]
+bar
+     : nat
+File "./output/captured_output.v", line 9, characters 26-29:
+The command has indeed failed with message:
+Illegal application (Non-functional construction): 
+The expression "0" of type "nat" cannot be applied to the term
+ "0" : "nat"
+File "./output/captured_output.v", line 11, characters 26-29:
+The command has indeed failed with message:
+Illegal application (Non-functional construction): 
+The expression "1" of type "nat" cannot be applied to the term
+ "1" : "nat"
+4
+     : nat
+File "./output/captured_output.v", line 16, characters 36-39:
+Warning: hello [warn-reference,user-warn,default]
+bar
+     : nat
+File "./output/captured_output.v", line 19, characters 0-52:
+Warning: Postfix notations (i.e. starting with a nonterminal symbol and
+ending with a terminal symbol) should usually be at level 1 (default).
+[postfix-notation-not-level-1,parsing,default]
+Captured output:
+0
+     : nat
+2
+     : nat
+hello
+[warn-reference,user-warn,default]
+bar
+     : nat
+The command has indeed failed with message:
+Illegal application (Non-functional construction): 
+The expression "0" of type "nat"
+cannot be applied to the term
+ "0" : "nat"
+hello [warn-reference,user-warn,default]
+bar
+     : nat
+hello [warn-reference,user-warn,default]
+bar
+     : nat
+Postfix notations (i.e. starting with a nonterminal symbol and ending with a
+terminal symbol) should usually be at level 1 (default).
+[postfix-notation-not-level-1,parsing,default]
+5
+     : nat
+Captured output:
+5
+     : nat
+File "./output/captured_output.v", line 31, characters 49-58:
+The command has indeed failed with message:
+Not OK: expected
+"5
+     : nat"
+Quickfix:
+Replace File "./output/captured_output.v", line 31, characters 49-58 with "5
+     : nat"
+File "./output/captured_output.v", line 34, characters 0-14:
+Output OK.
+File "./output/captured_output.v", line 38, characters 0-14:
+Output OK.
+File "./output/captured_output.v", line 41, characters 44-46:
+Output OK.

test-suite/output/captured_output.v

@@ -0,0 +1,41 @@
+Capture Output Check 0.
+Check 1.
+Capture Output Check 2.
+
+#[warn(note="hello")] Definition bar := 3.
+
+Capture Output Check bar.
+
+Capture Output Fail Check 0 0.
+
+Fail Capture Output Check 1 1.
+
+Succeed Capture Output Check 4.
+
+(* multiple captures add the output multiple times NOT interleaved *)
+Capture Output Capture Output Check bar.
+
+(* synterp message goes after the interp messages of previous commands *)
+Capture Output Reserved Notation "x !" (at level 2).
+
+Print Captured Output.
+
+Drop Captured Output.
+
+Capture Output Check 5.
+
+Succeed Drop Captured Output.
+
+Print Captured Output.
+
+Fail Assert Captured Output (printing width 102) "5 : nat".
+
+Assert Captured Output (printing width 102, no drop)
+"5
+     : nat".
+
+Assert Captured Output (printing width 102)
+"5
+     : nat".
+
+Assert Captured Output (printing width 102) "".

vernac/capturedOutput.ml

@@ -0,0 +1,86 @@
+(************************************************************************)
+(*         *      The Rocq Prover / The Rocq 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)         *)
+(************************************************************************)
+
+(* NB we could also keep the loc but it's unstable between coqtop
+   (proof general) and files so hard to use.Q
+
+   Could also add phase info, not sure if useful. *)
+type output = Message of Feedback.level * Pp.t
+
+type t = output list
+
+let from_rev_list l = List.rev l
+
+let from_list l = l
+
+type flags = {
+  width : int option;
+}
+
+let default_flags = {
+  width = None;
+}
+
+let parse_flag acc (flag : Vernacexpr.AssertCapturedOutputFlags.t CAst.t) =
+  match flag.v with
+  (* NoDrop handled outside this file *)
+  | NoDrop -> acc
+  | PrintingWidth w ->
+    if Option.has_some acc.width then
+      CErrors.user_err ?loc:flag.loc Pp.(str "Duplicate flag " ++ Ppvernac.pr_assert_captured_output_flag flag.v ++ str ".")
+    else { width = Some w }
+
+let parse_flags flags = List.fold_left parse_flag default_flags flags
+
+let buf = Buffer.create 117
+
+let pp_with_width w out =
+  let fmt = Format.formatter_of_buffer buf in
+  Topfmt.set_gp fmt { Topfmt.dflt_gp with margin = w };
+  Pp.pp_with fmt out;
+  Format.pp_print_flush fmt ();
+  Buffer.contents buf
+
+let pp_with_width w out =
+  Util.try_finally (fun () -> pp_with_width w out) ()
+    (fun () -> Buffer.reset buf) ()
+
+let print_captured_with_width w out =
+  let print_one (Message (_, msg)) = pp_with_width w msg in
+  let out = List.map print_one out in
+  String.concat "\n" out
+
+exception Mismatch of Loc.t option * string
+
+let () = CErrors.register_handler @@ function
+  | Mismatch (_,s) -> Some Pp.(str "Not OK: expected" ++ spc() ++ qstring s)
+  | _ -> None
+
+let () = Quickfix.register @@ function
+  | Mismatch (Some loc,s) -> [Quickfix.make ~loc (Pp.qstring s)]
+  | _ -> []
+
+let vernac_assert out flags {CAst.loc; v=s} =
+  let flags = parse_flags flags in
+  match flags.width with
+  | None -> CErrors.user_err Pp.(str "Explicit printing width required.")
+  | Some w ->
+    let out =
+      print_captured_with_width
+        (Option.default (Option.get @@ Topfmt.get_margin()) flags.width)
+        out
+    in
+    (* XXX trim? (remove whitespace at end of lines, remove empty line at begin/end) *)
+    if String.equal out s then Feedback.msg_info ?loc Pp.(str "Output OK.")
+    else
+      (* XXX make this an error by default warning so that it's easy
+         to see all output mismatch from a file? *)
+      (* TODO print in patch format? *)
+      Loc.raise ?loc (Mismatch (loc,out))

vernac/capturedOutput.mli

@@ -0,0 +1,24 @@
+(************************************************************************)
+(*         *      The Rocq Prover / The Rocq 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 output = Message of Feedback.level * Pp.t
+
+(** In chronological order *)
+type t = private output list
+
+(** Build a [t] from a list in reverse chronological order. *)
+val from_rev_list : output list -> t
+
+(** Build a [t] from a list in chronological order. *)
+val from_list : output list -> t
+
+(** [vernac_assert captured flags s] checks that [captured] matches [s] according to [flags]
+    ([NoDrop] is ignored and should be handled by the caller). *)
+val vernac_assert : t -> Vernacexpr.AssertCapturedOutputFlags.t CAst.t list -> string CAst.t -> unit