From a2e5414155ed8f589790ab627639e303ba1d6b3d Mon Sep 17 00:00:00 2001 From: Nicolas Osborne Date: Tue, 14 Nov 2023 10:25:31 +0100 Subject: [PATCH 1/3] Expose a quiet flag argument in registration This is general enough that different plugins would want to use it. --- bin/registration.ml | 3 +++ bin/registration.mli | 1 + 2 files changed, 4 insertions(+) diff --git a/bin/registration.ml b/bin/registration.ml index 81121fe0..4babeab8 100644 --- a/bin/registration.ml +++ b/bin/registration.ml @@ -25,6 +25,9 @@ let output_file = ~doc: "Print the generated code in OUTPUT. Overwrite the file if it exists.") +let quiet = + Arg.(value & flag & info [ "q"; "quiet" ] ~doc:"Don't print any warnings.") + let ocaml_file = let parse s = match Sys.file_exists s with diff --git a/bin/registration.mli b/bin/registration.mli index 63f42732..9c027677 100644 --- a/bin/registration.mli +++ b/bin/registration.mli @@ -7,3 +7,4 @@ val get_out_formatter : string option -> Format.formatter val setup_log : unit Cmdliner.Term.t val output_file : string option Cmdliner.Term.t val ocaml_file : string Cmdliner.Term.t +val quiet : bool Cmdliner.Term.t From d8d347bdcc03354e7d6fecc71c683de90c947b64 Mon Sep 17 00:00:00 2001 From: Nicolas Osborne Date: Tue, 14 Nov 2023 10:26:48 +0100 Subject: [PATCH 2/3] Add the quiet flag to ortac-qcheck-stm --- plugins/qcheck-stm/src/ortac_qcheck_stm.ml | 7 ++++--- plugins/qcheck-stm/src/reserr.ml | 5 +++-- plugins/qcheck-stm/src/reserr.mli | 2 +- 3 files changed, 8 insertions(+), 6 deletions(-) diff --git a/plugins/qcheck-stm/src/ortac_qcheck_stm.ml b/plugins/qcheck-stm/src/ortac_qcheck_stm.ml index b330a149..b9ca7a7f 100644 --- a/plugins/qcheck-stm/src/ortac_qcheck_stm.ml +++ b/plugins/qcheck-stm/src/ortac_qcheck_stm.ml @@ -4,10 +4,10 @@ module Ir_of_gospel = Ir_of_gospel module Reserr = Reserr module Stm_of_ir = Stm_of_ir -let main path init sut output () = +let main path init sut output quiet () = let open Reserr in let fmt = Registration.get_out_formatter output in - let pp = pp Ppxlib_ast.Pprintast.structure fmt in + let pp = pp quiet Ppxlib_ast.Pprintast.structure fmt in pp (let* sigs, config = Config.init path init sut in let* ir = Ir_of_gospel.run sigs config in @@ -40,7 +40,8 @@ end = struct let term = let open Registration in - Term.(const main $ ocaml_file $ init $ sut $ output_file $ setup_log) + Term.( + const main $ ocaml_file $ init $ sut $ output_file $ quiet $ setup_log) let cmd = Cmd.v info term end diff --git a/plugins/qcheck-stm/src/reserr.ml b/plugins/qcheck-stm/src/reserr.ml index 880f113e..50c004c6 100644 --- a/plugins/qcheck-stm/src/reserr.ml +++ b/plugins/qcheck-stm/src/reserr.ml @@ -220,12 +220,13 @@ let pp_kind ppf kind = let pp_errors = W.pp_param pp_kind level |> Fmt.list -let pp pp_ok ppf r = +let pp quiet pp_ok ppf r = let open Fmt in match r with | Ok a, warns -> ( pf ppf "%a@." pp_ok a; - match warns with [] -> () | warns -> pf stderr "%a@." pp_errors warns) + if not quiet then + match warns with [] -> () | warns -> pf stderr "%a@." pp_errors warns) | Error errs, warns -> pf stderr "%a@." pp_errors (errs @ warns) let sequence r = diff --git a/plugins/qcheck-stm/src/reserr.mli b/plugins/qcheck-stm/src/reserr.mli index 93bed454..a716a6dd 100644 --- a/plugins/qcheck-stm/src/reserr.mli +++ b/plugins/qcheck-stm/src/reserr.mli @@ -66,4 +66,4 @@ val fmap : ('a -> 'b) -> 'a reserr -> 'b reserr val ( <$> ) : ('a -> 'b) -> 'a reserr -> 'b reserr val app : ('a -> 'b) reserr -> 'a reserr -> 'b reserr val ( <*> ) : ('a -> 'b) reserr -> 'a reserr -> 'b reserr -val pp : 'a Fmt.t -> 'a reserr Fmt.t +val pp : bool -> 'a Fmt.t -> 'a reserr Fmt.t From 623de6de0efeb9a48d5ea33f0eabe1d578496165 Mon Sep 17 00:00:00 2001 From: Nicolas Osborne Date: Tue, 14 Nov 2023 10:40:24 +0100 Subject: [PATCH 3/3] Update changelog --- CHANGES.md | 2 ++ 1 file changed, 2 insertions(+) diff --git a/CHANGES.md b/CHANGES.md index f7a660d9..ac81493d 100644 --- a/CHANGES.md +++ b/CHANGES.md @@ -1,5 +1,7 @@ # Unreleased +- Add a quiet flag + [\#179](https://github.com/ocaml-gospel/ortac/pull/179) - Check for out of scope variables [\#175](https://github.com/ocaml-gospel/ortac/pull/175) - Translate constant integer patterns with a guard testing for equality