diff --git a/coqpp/coqpp_main.ml b/coqpp/coqpp_main.ml index ff3c74100ca7..2fd86e383ed7 100644 --- a/coqpp/coqpp_main.ml +++ b/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 diff --git a/doc/sphinx/proof-engine/vernacular-commands.rst b/doc/sphinx/proof-engine/vernacular-commands.rst index 7b8bfd7f96fb..76842807026e 100644 --- a/doc/sphinx/proof-engine/vernacular-commands.rst +++ b/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 diff --git a/doc/tools/docgram/common.edit_mlg b/doc/tools/docgram/common.edit_mlg index 8ab6b9c2165e..0a6fb025a991 100644 --- a/doc/tools/docgram/common.edit_mlg +++ b/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: [ diff --git a/doc/tools/docgram/fullGrammar b/doc/tools/docgram/fullGrammar index dd4fdea97af4..46094ebfb947 100644 --- a/doc/tools/docgram/fullGrammar +++ b/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 diff --git a/doc/tools/docgram/orderedGrammar b/doc/tools/docgram/orderedGrammar index bf3fca66453f..c08b33f4fd41 100644 --- a/doc/tools/docgram/orderedGrammar +++ b/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" diff --git a/test-suite/output/captured_output.out b/test-suite/output/captured_output.out new file mode 100644 index 000000000000..d049ea4b7edb --- /dev/null +++ b/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. diff --git a/test-suite/output/captured_output.v b/test-suite/output/captured_output.v new file mode 100644 index 000000000000..a1b8dcc46101 --- /dev/null +++ b/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) "". diff --git a/vernac/capturedOutput.ml b/vernac/capturedOutput.ml new file mode 100644 index 000000000000..215f0e518817 --- /dev/null +++ b/vernac/capturedOutput.ml @@ -0,0 +1,86 @@ +(************************************************************************) +(* * The Rocq Prover / The Rocq Development Team *) +(* v * Copyright INRIA, CNRS and contributors *) +(* 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)) diff --git a/vernac/capturedOutput.mli b/vernac/capturedOutput.mli new file mode 100644 index 000000000000..2876a3f56f8b --- /dev/null +++ b/vernac/capturedOutput.mli @@ -0,0 +1,24 @@ +(************************************************************************) +(* * The Rocq Prover / The Rocq Development Team *) +(* v * Copyright INRIA, CNRS and contributors *) +(* 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 diff --git a/vernac/g_vernac.mlg b/vernac/g_vernac.mlg index 8aca1f2d9134..afde3fd63bb4 100644 --- a/vernac/g_vernac.mlg +++ b/vernac/g_vernac.mlg @@ -55,7 +55,7 @@ let decl_notations = Entry.make "decl_notations" let record_field = Entry.make "record_field" let of_type = Entry.make "of_type" let of_type_inst = Entry.make "of_type_inst" -let section_subset_expr = Entry.make "section_subset_expr" +let section_subset_expr = Proof_using.section_subset_expr let scope_delimiter = Entry.make "scope_delimiter" let syntax_modifiers = Entry.make "syntax_modifiers" let goal_selector = Entry.make "goal_selector" @@ -105,6 +105,7 @@ GRAMMAR EXTEND Gram { CAst.make ~loc (ControlAllocLimit { kilowords = Int64.(mul (of_int n) mult) }) } | IDENT "Fail" -> { CAst.make ~loc ControlFail } | IDENT "Succeed" -> { CAst.make ~loc ControlSucceed } + | IDENT "Capture"; IDENT "Output" -> { CAst.make ~loc ControlCaptureOutput } ] ] ; decorated_vernac: @@ -1148,7 +1149,14 @@ GRAMMAR EXTEND Gram | IDENT "Remove"; table = IDENT; field = IDENT; v= LIST1 table_value -> { VernacSynPure (VernacRemoveOption ([table;field], v)) } | IDENT "Remove"; table = IDENT; v = LIST1 table_value -> - { VernacSynPure (VernacRemoveOption ([table], v)) } ]] + { VernacSynPure (VernacRemoveOption ([table], v)) } + | IDENT "Drop"; IDENT "Captured"; IDENT "Output" -> + { VernacSynPure VernacDropCapturedOutput } + | IDENT "Assert"; IDENT "Captured"; IDENT "Output"; + flags = OPT [ "("; flags = LIST0 captured_output_flag SEP ","; ")" -> { flags } ]; + s = lstring -> + { VernacSynPure (VernacAssertCapturedOutput (Option.default [] flags, s)) } + ]] ; query_command: [ [ IDENT "Eval"; r = red_expr; "in"; c = lconstr; "." -> @@ -1229,6 +1237,7 @@ GRAMMAR EXTEND Gram | IDENT "Strategies" -> { PrintStrategy None } | IDENT "Registered" -> { PrintRegistered } | IDENT "Registered"; IDENT "Schemes" -> { PrintRegisteredSchemes } + | IDENT "Captured"; IDENT "Output" -> { PrintCapturedOutput } ] ] ; debug_univ_name: @@ -1334,6 +1343,13 @@ GRAMMAR EXTEND Gram univ_name_list: [ [ "@{" ; l = LIST0 name; l' = OPT [ ";" ; l = LIST0 name -> { l } ] ; "}" -> { match l' with None -> [], l | Some l' -> l, l' } ] ] ; + captured_output_flag: + [ [ IDENT "no"; IDENT "drop" -> + { CAst.make ~loc AssertCapturedOutputFlags.NoDrop } + | IDENT "printing"; IDENT "width"; w = natural -> + { CAst.make ~loc @@ AssertCapturedOutputFlags.PrintingWidth w } + ] ] + ; END GRAMMAR EXTEND Gram diff --git a/vernac/ppvernac.ml b/vernac/ppvernac.ml index 70d723e65527..7e69481198cc 100644 --- a/vernac/ppvernac.ml +++ b/vernac/ppvernac.ml @@ -736,6 +736,11 @@ let pr_printable = function keyword "Print Notation" ++ spc() ++ str ntn_key | PrintNotation (Constrexpr.InCustomEntry ent, ntn_key) -> keyword "Print Notation" ++ spc() ++ pr_qualid ent ++ str ntn_key + | PrintCapturedOutput -> keyword "Print Captured Output" + +let pr_assert_captured_output_flag = let open AssertCapturedOutputFlags in function + | NoDrop -> str "no drop" + | PrintingWidth w -> str "printing width " ++ int w let pr_using e = let rec aux = function @@ -1321,6 +1326,14 @@ let pr_synpure_vernac_expr v = (keyword "Attributes" ++ spc () ++ pr_vernac_attributes attrs) ) + | VernacDropCapturedOutput -> return (keyword "Drop Captured Output") + | VernacAssertCapturedOutput (flags, {CAst.v=s}) -> + return ( + hov 2 + (keyword "Assert Captured Output" ++ spc() ++ + (if List.is_empty flags then mt() else + surround (prlist_with_sep spc (fun f -> pr_assert_captured_output_flag f.v) flags) ++ spc()) ++ + qstring s)) | VernacProof (None, None) -> return (keyword "Proof") | VernacProof (None, Some e) -> @@ -1472,6 +1485,7 @@ let pr_control_flag (p : control_flag) = | ControlAllocLimit n -> keyword "AllocLimit " ++ int64 Int64.(div n.kilowords 1000L) | ControlFail -> keyword "Fail" | ControlSucceed -> keyword "Succeed" + | ControlCaptureOutput -> keyword "Capture Output" in w ++ spc () diff --git a/vernac/ppvernac.mli b/vernac/ppvernac.mli index 37f44188347a..9c26a0b56898 100644 --- a/vernac/ppvernac.mli +++ b/vernac/ppvernac.mli @@ -33,3 +33,5 @@ val pr_vernac : Vernacexpr.vernac_control -> Pp.t (** Prints attributes, including surrounding "#[" "]", followed by space (empty on empty list) *) val pr_vernac_attributes : Attributes.vernac_flag list -> Pp.t + +val pr_assert_captured_output_flag : Vernacexpr.AssertCapturedOutputFlags.t -> Pp.t diff --git a/vernac/proof_using.ml b/vernac/proof_using.ml index c9d0366ab786..fcf125dcc6df 100644 --- a/vernac/proof_using.ml +++ b/vernac/proof_using.ml @@ -216,8 +216,9 @@ let suggest_variable env id = let value = ref None +let section_subset_expr = Procq.Entry.make "section_subset_expr" let using_to_string us = Pp.string_of_ppcmds (Ppvernac.pr_using us) -let entry = Procq.eoi_entry G_vernac.section_subset_expr +let entry = Procq.eoi_entry section_subset_expr let using_from_string us = Procq.Entry.parse entry (Procq.Parsable.make (Gramlib.Stream.of_string ("( "^us^" )"))) diff --git a/vernac/proof_using.mli b/vernac/proof_using.mli index 5f161860fbb9..e4cce50a97a4 100644 --- a/vernac/proof_using.mli +++ b/vernac/proof_using.mli @@ -35,3 +35,5 @@ val proof_using_opt_name : string list (** For the stm *) val using_from_string : string -> Vernacexpr.section_subset_expr + +val section_subset_expr : Vernacexpr.section_subset_expr Procq.Entry.t diff --git a/vernac/topfmt.ml b/vernac/topfmt.ml index b66f8a92c1b5..136f11859bb5 100644 --- a/vernac/topfmt.ml +++ b/vernac/topfmt.ml @@ -72,9 +72,6 @@ let _ = set_dflt_gp !std_ft let err_ft = ref Format.err_formatter let _ = set_gp !err_ft deep_gp -let deep_ft = ref (with_output_to stdout) -let _ = set_gp !deep_ft deep_gp - (* For parametrization through vernacular *) let default = Format.pp_get_max_boxes !std_ft () let default_margin = Format.pp_get_margin !std_ft () @@ -94,14 +91,12 @@ let set_margin v = let v = match v with None -> default_margin | Some v -> v in Format.pp_set_margin Format.str_formatter v; Format.pp_set_margin !std_ft v; - Format.pp_set_margin !deep_ft v; Format.pp_set_margin !err_ft v; (* Heuristic, based on usage: the column on the right of max_indent column is 20% of width, capped to 30 characters *) let m = max (64 * v / 100) (v-30) in Format.pp_set_max_indent Format.str_formatter m; Format.pp_set_max_indent !std_ft m; - Format.pp_set_max_indent !deep_ft m; Format.pp_set_max_indent !err_ft m (** Console display of feedback *) @@ -410,36 +405,32 @@ let print_err_exn any = std_logger ?pre_hdr Feedback.Error msg let with_output_to_file ~truncate fname func input = - let fname = String.concat "." [fname; "out"] in - let fullfname = System.get_output_path fname in - System.mkdir (Filename.dirname fullfname); - let channel = - let flags = [Open_wronly; Open_creat; Open_text] in - let flags = if truncate then Open_trunc :: flags else flags in - open_out_gen flags 0o666 fullfname + let acquire () = + let fname = String.concat "." [fname; "out"] in + let fullfname = System.get_output_path fname in + System.mkdir (Filename.dirname fullfname); + let channel = + let flags = [Open_wronly; Open_creat; Open_text] in + let flags = if truncate then Open_trunc :: flags else flags in + open_out_gen flags 0o666 fullfname + in + let old_fmt = !std_ft, !err_ft in + let new_ft = Format.formatter_of_out_channel channel in + set_gp new_ft (get_gp !std_ft); + old_fmt, new_ft, channel in - let old_fmt = !std_ft, !err_ft, !deep_ft in - let new_ft = Format.formatter_of_out_channel channel in - set_gp new_ft (get_gp !std_ft); - std_ft := new_ft; - err_ft := new_ft; - deep_ft := new_ft; - try - let output = func input in - std_ft := Util.pi1 old_fmt; - err_ft := Util.pi2 old_fmt; - deep_ft := Util.pi3 old_fmt; - Format.pp_print_flush new_ft (); - close_out channel; - output - with reraise -> - let reraise = Exninfo.capture reraise in - std_ft := Util.pi1 old_fmt; - err_ft := Util.pi2 old_fmt; - deep_ft := Util.pi3 old_fmt; + let scope (_, new_ft, channel) = + std_ft := new_ft; + err_ft := new_ft; + func input + in + let release (old_fmt, new_ft, channel) = + std_ft := fst old_fmt; + err_ft := snd old_fmt; Format.pp_print_flush new_ft (); close_out channel; - Exninfo.iraise reraise + in + Memprof_coq.Masking.with_resource ~acquire () ~scope ~release (* For coqtop -time, we display the position in the file, and a glimpse of the executed command *) diff --git a/vernac/topfmt.mli b/vernac/topfmt.mli index 3851a78971eb..e05ba00ffdd5 100644 --- a/vernac/topfmt.mli +++ b/vernac/topfmt.mli @@ -28,7 +28,6 @@ val with_output_to : out_channel -> Format.formatter val std_ft : Format.formatter ref val err_ft : Format.formatter ref -val deep_ft : Format.formatter ref (** {6 For parametrization through vernacular. } *) diff --git a/vernac/vernacControl.ml b/vernac/vernacControl.ml index da9678a64324..fa49084188de 100644 --- a/vernac/vernacControl.ml +++ b/vernac/vernacControl.ml @@ -47,6 +47,8 @@ type 'state control_entry = | ControlAllocLimit of { remaining : Control.kilowords; allocated : Control.kilowords } | ControlFail of { st : 'state } | ControlSucceed of { st : 'state } + | ControlCaptureOutput of { captured : CapturedOutput.output list; } + (** [captured] is in reverse chronological order. *) type 'state control_entries = 'state control_entry list @@ -214,6 +216,23 @@ let with_succeed ~with_local_state st0 f = let transient_st, v = with_local_state.with_local_state st0 f in Some (ControlSucceed { st = transient_st }, v) +(* XXX very naive capture means Flags.quiet is going to change results + also test_mode for Fail (but only affects loc if not Flags.quiet) *) +let with_capture ?loc:default_loc ~captured f = + let captured = ref captured in + let feeder (fb:Feedback.feedback) = match fb.contents with + | Message (lvl,_loc,_qf,msg) -> + captured := CapturedOutput.Message (lvl,msg) :: !captured + | _ -> () + in + let acquire () = Feedback.add_feeder feeder in + let scope _ = + let v = f () in + !captured, v + in + let release = Feedback.del_feeder in + Memprof_coq.Masking.with_resource ~acquire () ~scope ~release + let under_one_control ~loc ~with_local_state control f = match control with | ControlTime { duration } -> @@ -238,6 +257,9 @@ let under_one_control ~loc ~with_local_state control f = | ControlAllocLimit {remaining; allocated} -> with_alloc_limit ~limit:remaining ~allocated f | ControlFail {st} -> with_fail ~loc ~with_local_state st f | ControlSucceed {st} -> with_succeed ~with_local_state st f + | ControlCaptureOutput {captured} -> + let captured, v = with_capture ?loc ~captured f in + Some (ControlCaptureOutput {captured}, v) let rec under_control ~loc ~with_local_state controls ~noop f = match controls with @@ -248,33 +270,37 @@ let rec under_control ~loc ~with_local_state controls ~noop f = | Some (control, (rest,v)) -> control :: rest, v | None -> [], noop -let ignore_state = { with_local_state = fun _ f -> (), f () } - -let rec after_last_phase ~loc = function - | [] -> false +let finish push v = function + | ControlTime {duration} -> + Feedback.msg_notice @@ System.fmt_transaction_result (Ok ((),duration)); + Some v + | ControlInstructions {instructions} -> + Feedback.msg_notice @@ System.fmt_instructions_result (Ok ((),instructions)); + Some v + | ControlProfile {to_file; profstate} -> + Feedback.msg_notice @@ fmt_profile to_file (Ok ((),profstate)); + Some v + | ControlRedirect _ -> Some v + | ControlTimeout _ -> Some v + | ControlAllocLimit { remaining = _; allocated } -> + Feedback.msg_notice @@ fmt_allocated allocated; + Some v + | ControlFail _ -> CErrors.user_err Pp.(str "The command has not failed!") + | ControlSucceed _ -> None + | ControlCaptureOutput {captured} -> Some (push captured v) + +let rec last_under_control ~loc ~with_local_state ~push_captured controls ~noop f = + match controls with + | [] -> f() | control :: rest -> - (* don't match on [control] before processing [rest]: correctly handle eg [Fail Fail]. *) - let rest () = after_last_phase ~loc rest in - match under_one_control ~loc ~with_local_state:ignore_state control rest with - | None -> true - | Some (control,noop) -> - match control with - | ControlTime {duration} -> - Feedback.msg_notice @@ System.fmt_transaction_result (Ok ((),duration)); - noop - | ControlInstructions {instructions} -> - Feedback.msg_notice @@ System.fmt_instructions_result (Ok ((),instructions)); - noop - | ControlProfile {to_file; profstate} -> - Feedback.msg_notice @@ fmt_profile to_file (Ok ((),profstate)); - noop - | ControlRedirect _ -> noop - | ControlTimeout _ -> noop - | ControlAllocLimit { remaining = _; allocated } -> - Feedback.msg_notice @@ fmt_allocated allocated; - noop - | ControlFail _ -> CErrors.user_err Pp.(str "The command has not failed!") - | ControlSucceed _ -> true + let f () = last_under_control ~loc ~with_local_state ~push_captured rest ~noop f in + match under_one_control ~loc ~with_local_state control f with + | Some (control, v) -> + begin match finish push_captured v control with + | None -> noop + | Some v -> v + end + | None -> noop (** A global default timeout, controlled by option "Set Default Timeout n". Use "Unset Default Timeout" to deactivate it. *) @@ -315,5 +341,6 @@ let from_syntax_one : Vernacexpr.control_flag -> unit control_entry = fun flag - | ControlAllocLimit limit -> ControlAllocLimit { remaining = limit; allocated = { kilowords = 0L } } | ControlFail -> ControlFail { st = () } | ControlSucceed -> ControlSucceed { st = () } + | ControlCaptureOutput -> ControlCaptureOutput { captured = [] } let from_syntax control = List.map from_syntax_one (add_default_timeout control) diff --git a/vernac/vernacControl.mli b/vernac/vernacControl.mli index 1ba0a6377809..77098dc6936f 100644 --- a/vernac/vernacControl.mli +++ b/vernac/vernacControl.mli @@ -37,12 +37,18 @@ val under_control : loc:Loc.t option -> (unit -> 'b) -> 'state control_entries * 'b -(** Print any final messages (eg from [Time]) and raise final - exceptions (eg from [Fail] when the command did not fail). The - returned boolean tells if we should be noop ([Fail] where the - command failed or [Succeed] where it succeeded). +(** Like [under_control], also print any final messages (eg from + [Time]) and raise final exceptions (eg from [Fail] when the + command did not fail). + [output list] given to [push_captured] is in reverse chronological order. *) -val after_last_phase : loc:Loc.t option -> _ control_entries -> bool +val last_under_control : loc:Loc.t option -> + with_local_state:('state0,'state) with_local_state -> + push_captured:(CapturedOutput.output list -> 'b -> 'b) -> + 'state0 control_entries -> + noop:'b -> + (unit -> 'b) -> + 'b (** Exposed so that waterproof can change the error message. *) exception CmdTimeout diff --git a/vernac/vernac_classifier.ml b/vernac/vernac_classifier.ml index 986f87b852ec..4734820bef83 100644 --- a/vernac/vernac_classifier.ml +++ b/vernac/vernac_classifier.ml @@ -189,7 +189,11 @@ let classify_vernac e = | VernacSchemeEquality _ | VernacSchemeAll _ | VernacAddRewRule _ - | VernacDeclareInstance _ -> VtSideff ([], VtLater) + | VernacDeclareInstance _ + | VernacDropCapturedOutput + | VernacAssertCapturedOutput _ + -> VtSideff ([], VtLater) + (* Who knows *) | VernacOpenCloseScope _ | VernacDeclareScope _ | VernacDelimiters _ | VernacBindScope _ diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index 50fe68a8abe1..e095653d861c 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -2235,6 +2235,11 @@ let vernac_print_debug_delta qid = in Mod_subst.debug_pr_delta prc delta +let print_captured_output captured = + let pr_one (CapturedOutput.Message (_,msg)) = msg in + str "Captured output:" ++ fnl() ++ + prlist_with_sep fnl pr_one (List.rev captured) + let vernac_print = let no_state f = Vernactypes.(typed_vernac_gen ignore_state (fun _ -> no_state, f ())) @@ -2257,6 +2262,11 @@ let vernac_print = in typed_vernac_gen { ignore_state with proof = ReadOpt; opaque_access = Access } f in + let with_captured_output f = + let open Vernactypes in + let f {captured} = no_state, f captured in + typed_vernac_gen { ignore_state with captured = Read } f + in function | PrintTypingFlags -> with_proof_env @@ fun env _sigma -> pr_typing_flags (Environ.typing_flags env) | PrintTables -> no_state print_tables @@ -2335,6 +2345,7 @@ let vernac_print = | PrintStrategy r -> no_state @@ fun () -> print_strategy r | PrintRegistered -> no_state print_registered | PrintRegisteredSchemes -> no_state print_registered_schemes + | PrintCapturedOutput -> with_captured_output print_captured_output let vernac_search ~pstate ~atts s gopt r = let open ComSearch in @@ -2978,6 +2989,21 @@ let translate_pure_vernac ?loc ~atts v = let open Vernactypes in match v with vtdefault(fun () -> vernac_library_attributes atts) + | VernacDropCapturedOutput -> + vtconsumecapturedoutput (fun ~captured -> ()) + + | VernacAssertCapturedOutput (flags, s) -> + let f ~captured = CapturedOutput.(vernac_assert (from_rev_list captured) flags s) in + let nodrop = + List.exists (function + {CAst.v=AssertCapturedOutputFlags.NoDrop} -> true + | _ -> false) + flags + in + if nodrop then + vtreadcapturedoutput f + else vtconsumecapturedoutput f + (* Proof management *) | VernacFocus n -> vtmodifyproof(unsupported_attributes atts;vernac_focus n) diff --git a/vernac/vernacexpr.mli b/vernac/vernacexpr.mli index 1ba20ec8bdb5..e1826b5ed788 100644 --- a/vernac/vernacexpr.mli +++ b/vernac/vernacexpr.mli @@ -78,6 +78,7 @@ type printable = | PrintRegistered | PrintRegisteredSchemes | PrintNotation of qualid Constrexpr.notation_entry_gen * string + | PrintCapturedOutput type glob_search_where = InHyp | InConcl | Anywhere @@ -366,6 +367,12 @@ type hints_expr = | HintsConstructors of Libnames.qualid list | HintsExtern of int * Constrexpr.constr_expr option * Gentactic.raw_generic_tactic +module AssertCapturedOutputFlags : sig + type t = + | NoDrop + | PrintingWidth of int +end + (** [synterp_vernac_expr] describes the AST of commands which have effects on parsing or parsing extensions *) type synterp_vernac_expr = @@ -493,6 +500,8 @@ type nonrec synpure_vernac_expr = | VernacPrimitive of ident_decl * CPrimitives.op_or_type * constr_expr option | VernacComments of comment list | VernacAttributes of Attributes.vernac_flags + | VernacDropCapturedOutput + | VernacAssertCapturedOutput of AssertCapturedOutputFlags.t CAst.t list * lstring (* Proof management *) | VernacAbort @@ -532,6 +541,7 @@ type control_flag_r = | ControlAllocLimit of Control.kilowords | ControlFail | ControlSucceed + | ControlCaptureOutput type control_flag = control_flag_r CAst.t diff --git a/vernac/vernacinterp.ml b/vernac/vernacinterp.ml index 1756496b37dc..51991290206e 100644 --- a/vernac/vernacinterp.ml +++ b/vernac/vernacinterp.ml @@ -30,30 +30,35 @@ let with_interp_state ~unfreeze_transient st = in { VernacControl.with_local_state } +let push_captured captured (st:Vernacstate.explicit_state) = { + st with + captured_output = CList.append captured st.captured_output; +} + let interp_control_gen ~loc ~st ~unfreeze_transient control f = - let noop = st.Vernacstate.interp.lemmas, st.Vernacstate.interp.program in - let control, res = - VernacControl.under_control ~loc - ~with_local_state:(with_interp_state ~unfreeze_transient st) - control - ~noop - (Flags.with_modified_ref Flags.in_synterp_phase (fun _ -> Some false) f) - in - if VernacControl.after_last_phase ~loc control - then noop - else res + let noop = Vernacstate.explicit_from_frozen st.Vernacstate.interp in + VernacControl.last_under_control ~loc + ~with_local_state:(with_interp_state ~unfreeze_transient st) + ~push_captured + control + ~noop + (* XXX is there a reason we only modify under the controls instead of around them? *) + (Flags.with_modified_ref Flags.in_synterp_phase (fun _ -> Some false) f) (* [loc] is the [Loc.t] of the vernacular command being interpreted. *) let rec interp_expr ?loc ~st cmd = let before_univs = Global.universes () in - let pstack, pm = with_generic_atts ~check:false cmd.attrs (fun ~atts -> + let extra = with_generic_atts ~check:false cmd.attrs (fun ~atts -> interp_expr_core ?loc ~atts ~st cmd.expr) in let after_univs = Global.universes () in - if before_univs == after_univs then pstack, pm - else - let f = Declare.Proof.update_sigma_univs after_univs in - Option.map (Vernacstate.LemmaStack.map ~f) pstack, pm + let pstack = + if before_univs == after_univs then extra.Vernacstate.proof + else + let f = Declare.Proof.update_sigma_univs after_univs in + Option.map (Vernacstate.LemmaStack.map ~f) extra.proof + in + { extra with proof = pstack } and interp_expr_core ?loc ~atts ~st c = match c with @@ -75,35 +80,27 @@ and interp_expr_core ?loc ~atts ~st c = | v -> let fv = Vernacentries.translate_vernac ?loc ~atts v in - let stack = st.Vernacstate.interp.lemmas in - let program = st.Vernacstate.interp.program in - let {Vernactypes.prog; proof; opaque_access=(); }, () = Vernactypes.run ?loc fv { - prog=program; - proof=stack; - opaque_access=(); - } - in - proof, prog + let extra, () = Vernactypes.run ?loc fv (Vernacstate.explicit_from_frozen st.Vernacstate.interp) in + extra and vernac_load ~verbosely entries = (* Note that no proof should be open here, so the state here is just token for now *) let st = Vernacstate.freeze_full_state () in let v_mod = if verbosely then Flags.verbosely else Flags.silently in - let interp_entry (stack, pm) (CAst.{ loc; v = cmd }, synterp_st) = + let interp_entry extra_state (CAst.{ loc; v = cmd }, synterp_st) = Vernacstate.Synterp.unfreeze synterp_st; - let st = Vernacstate.{ synterp = synterp_st; interp = { st.interp with Interp.lemmas = stack; program = pm }} in + let st = Vernacstate.{ synterp = synterp_st; interp = Vernacstate.set_explicit_in_frozen st.interp extra_state } in v_mod (interp_control ~st) (CAst.make ?loc cmd) in - let pm = st.Vernacstate.interp.program in - let stack = st.Vernacstate.interp.lemmas in - let stack, pm = + let extra = Vernacstate.explicit_from_frozen st.interp in + let extra = Dumpglob.with_glob_output Dumpglob.NoGlob - (fun () -> List.fold_left interp_entry (stack, pm) entries) () + (fun () -> List.fold_left interp_entry extra entries) () in (* If Load left a proof open, we fail too. *) - if Option.has_some stack then + if Option.has_some extra.proof then CErrors.user_err Pp.(str "Files processed by Load cannot leave open proofs."); - stack, pm + extra and interp_control ~st ({ CAst.v = cmd; loc }) = Util.try_finally (fun () -> @@ -135,7 +132,7 @@ let interp_qed_delayed ~proof ~st pe = pm) pm in - stack, pm + { (Vernacstate.explicit_from_frozen st.interp) with proof = stack; prog = pm; } let interp_qed_delayed_control ~proof ~st ~control { CAst.loc; v=pe } = interp_control_gen ~loc ~st control diff --git a/vernac/vernacstate.ml b/vernac/vernacstate.ml index eb339bd12cbb..91c10c629d90 100644 --- a/vernac/vernacstate.ml +++ b/vernac/vernacstate.ml @@ -100,6 +100,7 @@ end let s_cache = ref None let s_lemmas = ref None let s_program = ref (NeList.singleton Declare.OblState.empty) +let s_captured = ref [] module Interp = struct @@ -110,6 +111,7 @@ type t = { lemmas : LemmaStack.t option; (* proofs of lemmas currently opened *) program : Declare.OblState.t NeList.t; (* obligations table *) opaques : Opaques.Summary.t; (* opaque proof terms *) + captured_output : CapturedOutput.output list; (* output is in reverse chronological order *) } let invalidate_cache () = @@ -132,15 +134,17 @@ let freeze_interp_state () = lemmas = !s_lemmas; program = !s_program; opaques = Opaques.Summary.freeze (); + captured_output = !s_captured; } let make_shallow s = { s with system = System.Stm.make_shallow s.system } -let unfreeze_interp_state { system; lemmas; program; opaques } = +let unfreeze_interp_state { system; lemmas; program; opaques; captured_output } = do_if_not_cached s_cache System.unfreeze system; s_lemmas := lemmas; s_program := program; + s_captured := captured_output; Opaques.Summary.unfreeze opaques end @@ -161,14 +165,34 @@ let unfreeze_full_state st = Interp.unfreeze_interp_state st.interp) () +type explicit_state = { + proof : LemmaStack.t option; + prog : Declare.OblState.t NeList.t; + captured_output : CapturedOutput.output list; +} + +let explicit_from_frozen st = { + proof = st.Interp.lemmas; + prog = st.program; + captured_output = st.captured_output; +} + +let set_explicit_in_frozen st v = { + st with + Interp.lemmas = v.proof; + program = v.prog; + captured_output = v.captured_output; +} + (* Compatibility module *) module Declare_ = struct let get_program () = !s_program - let set (pstate,pm) = - s_lemmas := pstate; - s_program := pm + let set v = + s_lemmas := v.proof; + s_program := v.prog; + s_captured := v.captured_output let get_pstate () = Option.map (LemmaStack.with_top ~f:(fun x -> x)) !s_lemmas diff --git a/vernac/vernacstate.mli b/vernac/vernacstate.mli index 1886c38cd1cf..79a934fc7b30 100644 --- a/vernac/vernacstate.mli +++ b/vernac/vernacstate.mli @@ -57,6 +57,8 @@ module Interp : sig (** program mode table. One per open module/section including the toplevel module. *) ; opaques : Opaques.Summary.t (** qed-terminated proofs *) + ; captured_output : CapturedOutput.output list + (** output is in reverse chronological order *) } val freeze_interp_state : unit -> t @@ -75,6 +77,16 @@ type t = val freeze_full_state : unit -> t val unfreeze_full_state : t -> unit +(** States which are mostly handled functionally. *) +type explicit_state = { + proof : LemmaStack.t option; + prog : Declare.OblState.t NeList.t; + captured_output : CapturedOutput.output list; +} + +val explicit_from_frozen : Interp.t -> explicit_state +val set_explicit_in_frozen : Interp.t -> explicit_state -> Interp.t + (** STM-specific state handling *) module Stm : sig @@ -133,7 +145,7 @@ module Declare : sig (* Low-level stuff *) val get_program : unit -> Declare.OblState.t NeList.t - val set : LemmaStack.t option * Declare.OblState.t NeList.t -> unit + val set : explicit_state -> unit val get_pstate : unit -> Declare.Proof.t option diff --git a/vernac/vernactypes.ml b/vernac/vernactypes.ml index de650bdabcf1..7e502a215b82 100644 --- a/vernac/vernactypes.ml +++ b/vernac/vernactypes.ml @@ -114,6 +114,23 @@ module Proof = struct end +module Captured = struct + type state = CapturedOutput.output list + + type _ t = + | Ignore : unit t + | Read : state t + | Consume : state t + + let runner (type a) (ty:a t) : (a,unit,state) runner = + { run = fun ?loc captured f -> + match ty with + | Ignore -> let (), v = f () in captured, v + | Read -> let (), v = f captured in captured, v + | Consume -> let (), v = f captured in [], v + } +end + module OpaqueAccess = struct (* Modification of opaque tables (by Require registering foreign @@ -146,26 +163,38 @@ let combine_runners (type a b x c d y) (r1:(a,b,x) runner) (r2:(c,d,y) runner) with (y, (b, o)) -> (b, (y, o)) with (x, (y, o)) -> ((x, y), o) } -type ('prog,'proof,'opaque_access) state_gen = { +type ('prog,'proof,'captured,'opaque_access) state_gen = { prog : 'prog; proof : 'proof; + captured : 'captured; opaque_access : 'opaque_access; } -let tuple { prog; proof; opaque_access } = (prog, proof), opaque_access -let untuple ((prog, proof), opaque_access) = { prog; proof; opaque_access } +let tuple { prog; proof; captured; opaque_access } = prog, (proof, (captured, opaque_access)) +let untuple (prog, (proof, (captured, opaque_access))) = { prog; proof; captured; opaque_access } + +let tuple_explicit (st:Vernacstate.explicit_state) = st.prog, (st.proof, (st.captured_output, ())) +let untuple_explicit (prog, (proof, (captured_output, ()))) : Vernacstate.explicit_state = + { prog; proof; captured_output } -type no_state = (unit, unit, unit) state_gen -let no_state = { prog = (); proof = (); opaque_access = (); } +type no_state = (unit, unit, unit, unit) state_gen +let no_state = { prog = (); proof = (); captured = (); opaque_access = (); } -let ignore_state = { prog = Prog.Ignore; proof = Proof.Ignore; opaque_access = OpaqueAccess.Ignore } +let ignore_state = { + prog = Prog.Ignore; + proof = Proof.Ignore; + captured = Captured.Ignore; + opaque_access = OpaqueAccess.Ignore; +} type 'r typed_vernac_gen = TypedVernac : { spec : (('inprog, 'outprog) Prog.t, ('inproof, 'outproof) Proof.t, + 'incaptured Captured.t, 'inaccess OpaqueAccess.t) state_gen; - run : ('inprog, 'inproof, 'inaccess) state_gen -> ('outprog, 'outproof, unit) state_gen * 'r; + run : ('inprog, 'inproof, 'incaptured, 'inaccess) state_gen -> + ('outprog, 'outproof, unit, unit) state_gen * 'r; } -> 'r typed_vernac_gen let map_typed_vernac f (TypedVernac {spec; run}) = @@ -173,15 +202,20 @@ let map_typed_vernac f (TypedVernac {spec; run}) = type typed_vernac = unit typed_vernac_gen -type full_state = (Prog.stack,Vernacstate.LemmaStack.t option,unit) state_gen - -let run ?loc (TypedVernac { spec = { prog; proof; opaque_access }; run }) (st:full_state) : full_state * _ = - let ( * ) = combine_runners in - let runner = Prog.runner prog * Proof.runner proof * OpaqueAccess.runner opaque_access in - let st, v = runner.run ?loc (tuple st) @@ fun st -> - let st, v= run @@ untuple st in tuple st, v +let run ?loc (TypedVernac { spec = { prog; proof; captured; opaque_access }; run }) + (st:Vernacstate.explicit_state) : Vernacstate.explicit_state * _ = + (* NB: [@] is right associative *) + let ( @ ) = combine_runners in + let runner = + Prog.runner prog + @ Proof.runner proof + @ Captured.runner captured + @ OpaqueAccess.runner opaque_access in - untuple st, v + let st, v = runner.run ?loc (tuple_explicit st) @@ fun st -> + let st, v = run @@ untuple st in tuple st, v + in + untuple_explicit st, v let typed_vernac_gen spec run = TypedVernac { spec; run } @@ -224,3 +258,9 @@ let vtopenproofprogram f = typed_vernac { ignore_state with prog = Modify; proof let vtopaqueaccess f = typed_vernac { ignore_state with opaque_access = Access } (fun {opaque_access} -> let () = f ~opaque_access in no_state) + +let vtreadcapturedoutput f = typed_vernac { ignore_state with captured = Read } + (fun {captured} -> let () = f ~captured in no_state) + +let vtconsumecapturedoutput f = typed_vernac { ignore_state with captured = Consume } + (fun {captured} -> let () = f ~captured in no_state) diff --git a/vernac/vernactypes.mli b/vernac/vernactypes.mli index 7488e8f6b847..93684ec93f95 100644 --- a/vernac/vernactypes.mli +++ b/vernac/vernactypes.mli @@ -34,50 +34,76 @@ module Proof : sig | Open : (unit, state) t end +module Captured : sig + type state = CapturedOutput.output list + (** In reverse chronological order *) + + (** No write: currently always done through controls instead of the command itself. *) + type _ t = + | Ignore : unit t + | Read : state t + | Consume : state t +end + module OpaqueAccess : sig type _ t = | Ignore : unit t | Access : Global.indirect_accessor t end -type ('prog,'proof,'opaque_access) state_gen = { +type ('prog,'proof,'captured,'opaque_access) state_gen = { prog : 'prog; proof : 'proof; + captured : 'captured; opaque_access : 'opaque_access; } -type no_state = (unit, unit, unit) state_gen +type no_state = (unit, unit, unit, unit) state_gen val no_state : no_state (** Useful for patterns like [{ no_state with proof = newproof }] when modifying a subset of the state. *) -val ignore_state : ((unit, unit) Prog.t, (unit, unit) Proof.t, unit OpaqueAccess.t) state_gen +val ignore_state : + ((unit, unit) Prog.t, + (unit, unit) Proof.t, + unit Captured.t, + unit OpaqueAccess.t) + state_gen type 'r typed_vernac_gen = TypedVernac : { spec : (('inprog, 'outprog) Prog.t, ('inproof, 'outproof) Proof.t, + 'incaptured Captured.t, 'inaccess OpaqueAccess.t) state_gen; - run : ('inprog, 'inproof, 'inaccess) state_gen -> ('outprog, 'outproof, unit) state_gen * 'r; + run : ('inprog, 'inproof, 'incaptured, 'inaccess) state_gen -> + ('outprog, 'outproof, unit, unit) state_gen * 'r; } -> 'r typed_vernac_gen type typed_vernac = unit typed_vernac_gen val typed_vernac_gen - : (('inprog, 'outprog) Prog.t, ('inproof, 'outproof) Proof.t, 'inaccess OpaqueAccess.t) state_gen - -> (('inprog, 'inproof, 'inaccess) state_gen -> ('outprog, 'outproof, unit) state_gen * 'r) + : (('inprog, 'outprog) Prog.t, + ('inproof, 'outproof) Proof.t, + 'incaptured Captured.t, + 'inaccess OpaqueAccess.t) state_gen + -> (('inprog, 'inproof, 'incaptured, 'inaccess) state_gen -> + ('outprog, 'outproof, unit, unit) state_gen * 'r) -> 'r typed_vernac_gen val map_typed_vernac : ('a -> 'b) -> 'a typed_vernac_gen -> 'b typed_vernac_gen val typed_vernac - : (('inprog, 'outprog) Prog.t, ('inproof, 'outproof) Proof.t, 'inaccess OpaqueAccess.t) state_gen - -> (('inprog, 'inproof, 'inaccess) state_gen -> ('outprog, 'outproof, unit) state_gen) + : (('inprog, 'outprog) Prog.t, + ('inproof, 'outproof) Proof.t, + 'incaptured Captured.t, + 'inaccess OpaqueAccess.t) state_gen + -> (('inprog, 'inproof, 'incaptured, 'inaccess) state_gen -> + ('outprog, 'outproof, unit, unit) state_gen) -> typed_vernac -type full_state = (Prog.stack, Vernacstate.LemmaStack.t option, unit) state_gen - -val run : ?loc:Loc.t -> 'r typed_vernac_gen -> full_state -> full_state * 'r +val run : ?loc:Loc.t -> 'r typed_vernac_gen -> + Vernacstate.explicit_state -> Vernacstate.explicit_state * 'r (** Some convenient typed_vernac constructors. Used by coqpp. *) @@ -93,3 +119,5 @@ val vtmodifyprogram : (pm:Declare.OblState.t -> Declare.OblState.t) -> typed_ver val vtdeclareprogram : (pm:Declare.OblState.t -> Declare.Proof.t) -> typed_vernac val vtopenproofprogram : (pm:Declare.OblState.t -> Declare.OblState.t * Declare.Proof.t) -> typed_vernac val vtopaqueaccess : (opaque_access:Global.indirect_accessor -> unit) -> typed_vernac +val vtreadcapturedoutput : (captured:Captured.state -> unit) -> typed_vernac +val vtconsumecapturedoutput : (captured:Captured.state -> unit) -> typed_vernac