From 76401a8d17fe220e340bdd8314e59a9776e23445 Mon Sep 17 00:00:00 2001 From: Andrew Helwer Date: Mon, 13 Oct 2025 12:03:02 -0700 Subject: [PATCH 01/11] Added unit tests for CLI args Signed-off-by: Andrew Helwer --- src/tlapm_args.ml | 125 +++++++++++++++++++++++++++++++++++++++++---- src/tlapm_args.mli | 8 ++- src/tlapm_lib.ml | 4 +- 3 files changed, 124 insertions(+), 13 deletions(-) diff --git a/src/tlapm_args.ml b/src/tlapm_args.ml index 48c8599d3..2af410ec3 100644 --- a/src/tlapm_args.ml +++ b/src/tlapm_args.ml @@ -53,10 +53,11 @@ let set_default_method meth = (* FIXME use Arg.parse instead *) -let parse_args args opts mods usage_fmt = +let parse_args executable_name args opts mods usage_fmt = try - Arg.parse_argv (Array.of_list args) opts (fun mfile -> mods := mfile :: !mods) - (Printf.sprintf usage_fmt (Filename.basename Sys.executable_name)) + Arg.current := 0; + Arg.parse_argv args opts (fun mfile -> mods := mfile :: !mods) + (Printf.sprintf usage_fmt (Filename.basename executable_name)) with Arg.Bad msg -> print_endline msg ; flush stdout ; @@ -134,7 +135,7 @@ let quote_if_needed s = end -let init () = +let init (executable_name : string) (args : string array) = let mods = ref [] in let helpfn = ref (fun () -> ()) in let show_help () = !helpfn () in @@ -246,13 +247,12 @@ let init () = in helpfn := begin fun () -> Arg.usage opts - (Printf.sprintf usage_fmt (Filename.basename Sys.executable_name)) ; + (Printf.sprintf usage_fmt (Filename.basename executable_name)) ; exit 0 end ; - let args = Array.to_list Sys.argv in - parse_args args opts mods usage_fmt ; + parse_args executable_name args opts mods usage_fmt ; if !show_config || !verbose then begin - print_endline (printconfig true) ; + (*print_endline (printconfig true) ;*) flush stdout end ; if !show_config then exit 0 ; @@ -260,7 +260,7 @@ let init () = Arg.usage opts (Printf.sprintf "Need at least one module file.\n\n\ Usage: %s FILE ...\noptions are:" - (Filename.basename Sys.executable_name)) ; + (Filename.basename executable_name)) ; exit 2 end ; if !summary then begin @@ -276,7 +276,7 @@ let init () = (tm.Unix.tm_year + 1900) (tm.Unix.tm_mon + 1) tm.Unix.tm_mday tm.Unix.tm_hour tm.Unix.tm_min tm.Unix.tm_sec; Printf.printf " with command line:\n\\*"; - Array.iter (fun s -> Printf.printf " %s" (quote_if_needed s)) Sys.argv; + Array.iter (fun s -> Printf.printf " %s" (quote_if_needed s)) args; Printf.printf "\n\n%!" end; if !use_stdin && (List.length !mods) <> 1 then begin @@ -286,3 +286,108 @@ let init () = exit 2 end; !mods + +(** Unit tests to ensure CLI parameter format does not change. +*) + +type setting = [`B of bool | `I of int | `S of string] + +let settings = [ + (`B Params.toolbox, `B !Params.toolbox); + (`I Params.toolbox_vsn, `I !Params.toolbox_vsn); +] + +type setting_value = [ + `B of string * bool ref * bool + | `I of string * int ref * int + | `F of string * float ref * float + | `S of string * string ref * string + | `SO of string * string option ref * string option +] + +let display_setting_value (v : setting_value) : string = + match v with + | `B (n, rf, v) -> Printf.sprintf "%s: %b [%b]" n v !rf + | `I (n, rf, v) -> Printf.sprintf "%s: %d [%d]" n v !rf + | `F (n, rf, v) -> Printf.sprintf "%s: %f [%f]" n v !rf + | `S (n, rf, v) -> Printf.sprintf "%s: %s [%s]" n v !rf + | `SO (n, rf, v) -> Printf.sprintf "%s: %s [%s]" n (Option.default "None" v) (Option.default "None" !rf) + +let setting_values () : setting_value list = [ + `B ("toolbox", Params.toolbox, !Params.toolbox); + `I ("toolbox_vsn", Params.toolbox_vsn, !Params.toolbox_vsn); + `B ("use_stdin", Params.use_stdin, !Params.use_stdin); + `B ("prefer_stdlib", Params.prefer_stdlib, !Params.prefer_stdlib); + `B ("notl", Params.notl, !Params.notl); + `B ("verbose", Params.verbose, !Params.verbose); + `B ("check", Params.check, !Params.check); + `S ("output_dir", Params.output_dir, !Params.output_dir); + `I ("wait", Params.wait, !Params.wait); + `B ("no_fp", Params.no_fp, !Params.no_fp); + `I ("nofp_sl", Params.nofp_sl, !Params.nofp_sl); + `I ("nofp_el", Params.nofp_el, !Params.nofp_el); + `B ("printallobs", Params.printallobs, !Params.printallobs); + `B ("pr_normal", Params.pr_normal, !Params.pr_normal); + `B ("ob_flatten", Params.ob_flatten, !Params.ob_flatten); + `B ("noproving", Params.noproving, !Params.noproving); + `S ("fp_hist_dir", Params.fp_hist_dir, !Params.fp_hist_dir); + `I ("fp_original_number", Params.fp_original_number, !Params.fp_original_number); + `B ("safefp", Params.safefp, !Params.safefp); + `B ("fp_deb", Params.fp_deb, !Params.fp_deb); + `B ("use_xtla", Params.use_xtla, !Params.use_xtla); + `B ("xtla", Params.xtla, !Params.xtla); + `I ("tb_sl", Params.tb_sl, !Params.tb_sl); + `I ("tb_el", Params.tb_el, !Params.tb_el); + `B ("cleanfp", Params.cleanfp, !Params.cleanfp); + `SO ("fpf_in", Params.fpf_in, !Params.fpf_in); + `SO ("fpf_out", Params.fpf_out, !Params.fpf_out); + `B ("fp_loaded", Params.fp_loaded, !Params.fp_loaded); + `B ("summary", Params.summary, !Params.summary); + `B ("stats", Params.stats, !Params.stats); + `B ("keep_going", Params.keep_going, !Params.keep_going); + `B ("suppress_all", Params.suppress_all, !Params.suppress_all); + `F ("timeout_stretch", Params.timeout_stretch, !Params.timeout_stretch); + `F ("backend_timeout", Params.backend_timeout, !Params.backend_timeout); +] + +let default_setting_values = setting_values () + +let setting_value_changed = + (fun (setting : setting_value) -> + match setting with + | `B (_, rf, v) -> not (!rf = v) + | `I (_, rf, v) -> not (!rf = v) + | `F (_, rf, v) -> not (!rf = v) + | `S (_, rf, v) -> not (!rf = v) + | `SO (_, rf, v) -> not (!rf = v) + ) + +let set_setting_value = + (fun (setting : setting_value) -> + match setting with + | `B (_, rf, v) -> rf := v + | `I (_, rf, v) -> rf := v + | `F (_, rf, v) -> rf := v + | `S (_, rf, v) -> rf := v + | `SO (_, rf, v) -> rf := v + ) + +let reset_setting_values () = List.iter set_setting_value default_setting_values + +let changed_setting_values () = List.filter setting_value_changed default_setting_values + +let%test "basic" = + reset_setting_values (); + init "tlapm" [|"tlapm"; "Test.tla";|] = ["Test.tla"] + && changed_setting_values () = [] + +let%test "verbose_short" = + reset_setting_values (); + init "tlapm" [|"tlapm"; "-v"; "Test.tla";|] = ["Test.tla"] + && changed_setting_values () = [`B ("verbose", Params.verbose, false)] + +let%test "verbose_long" = + reset_setting_values (); + init "tlapm" [|"tlapm"; "--verbose"; "Test.tla";|] = ["Test.tla"] + && changed_setting_values () = [`B ("verbose", Params.verbose, false)] + diff --git a/src/tlapm_args.mli b/src/tlapm_args.mli index 550a04f0a..ec5c92751 100644 --- a/src/tlapm_args.mli +++ b/src/tlapm_args.mli @@ -2,4 +2,10 @@ Copyright (C) 2011 INRIA and Microsoft Corporation *) -val init: unit -> string list + +(** Given the executable name and an array of command-line arguments, parses + those arguments then either sets associated values in the Params module + or directly takes action such as printing out file contents or deleting + directories. Returns a list of files for proof checking. +*) +val init: string -> string array -> string list diff --git a/src/tlapm_lib.ml b/src/tlapm_lib.ml index a328d9ae6..4bd57a162 100644 --- a/src/tlapm_lib.ml +++ b/src/tlapm_lib.ml @@ -586,9 +586,9 @@ let init () = Printexc.record_backtrace true; Format.pp_set_max_indent Format.err_formatter 35; if Params.debugging "main" then - main (Tlapm_args.init ()) + main (Tlapm_args.init Sys.executable_name Sys.argv) else - try main (Tlapm_args.init ()) with + try main (Tlapm_args.init Sys.executable_name Sys.argv) with | Errors.Fatal -> Util.eprintf "tlapm: Exiting because of the above error."; exit 0; From a574a5e037a96f8520fbb0888c4e6eccbc29190a Mon Sep 17 00:00:00 2001 From: Andrew Helwer Date: Tue, 21 Oct 2025 16:35:45 -0700 Subject: [PATCH 02/11] Moved CLI unit tests to test directory Signed-off-by: Andrew Helwer --- src/tlapm_args.ml | 105 --------------------------------- test/cli/cli_tests.ml | 134 ++++++++++++++++++++++++++++++++++++++++++ test/cli/dune | 5 ++ 3 files changed, 139 insertions(+), 105 deletions(-) create mode 100644 test/cli/cli_tests.ml create mode 100644 test/cli/dune diff --git a/src/tlapm_args.ml b/src/tlapm_args.ml index 2af410ec3..d4e66dabb 100644 --- a/src/tlapm_args.ml +++ b/src/tlapm_args.ml @@ -286,108 +286,3 @@ let init (executable_name : string) (args : string array) = exit 2 end; !mods - -(** Unit tests to ensure CLI parameter format does not change. -*) - -type setting = [`B of bool | `I of int | `S of string] - -let settings = [ - (`B Params.toolbox, `B !Params.toolbox); - (`I Params.toolbox_vsn, `I !Params.toolbox_vsn); -] - -type setting_value = [ - `B of string * bool ref * bool - | `I of string * int ref * int - | `F of string * float ref * float - | `S of string * string ref * string - | `SO of string * string option ref * string option -] - -let display_setting_value (v : setting_value) : string = - match v with - | `B (n, rf, v) -> Printf.sprintf "%s: %b [%b]" n v !rf - | `I (n, rf, v) -> Printf.sprintf "%s: %d [%d]" n v !rf - | `F (n, rf, v) -> Printf.sprintf "%s: %f [%f]" n v !rf - | `S (n, rf, v) -> Printf.sprintf "%s: %s [%s]" n v !rf - | `SO (n, rf, v) -> Printf.sprintf "%s: %s [%s]" n (Option.default "None" v) (Option.default "None" !rf) - -let setting_values () : setting_value list = [ - `B ("toolbox", Params.toolbox, !Params.toolbox); - `I ("toolbox_vsn", Params.toolbox_vsn, !Params.toolbox_vsn); - `B ("use_stdin", Params.use_stdin, !Params.use_stdin); - `B ("prefer_stdlib", Params.prefer_stdlib, !Params.prefer_stdlib); - `B ("notl", Params.notl, !Params.notl); - `B ("verbose", Params.verbose, !Params.verbose); - `B ("check", Params.check, !Params.check); - `S ("output_dir", Params.output_dir, !Params.output_dir); - `I ("wait", Params.wait, !Params.wait); - `B ("no_fp", Params.no_fp, !Params.no_fp); - `I ("nofp_sl", Params.nofp_sl, !Params.nofp_sl); - `I ("nofp_el", Params.nofp_el, !Params.nofp_el); - `B ("printallobs", Params.printallobs, !Params.printallobs); - `B ("pr_normal", Params.pr_normal, !Params.pr_normal); - `B ("ob_flatten", Params.ob_flatten, !Params.ob_flatten); - `B ("noproving", Params.noproving, !Params.noproving); - `S ("fp_hist_dir", Params.fp_hist_dir, !Params.fp_hist_dir); - `I ("fp_original_number", Params.fp_original_number, !Params.fp_original_number); - `B ("safefp", Params.safefp, !Params.safefp); - `B ("fp_deb", Params.fp_deb, !Params.fp_deb); - `B ("use_xtla", Params.use_xtla, !Params.use_xtla); - `B ("xtla", Params.xtla, !Params.xtla); - `I ("tb_sl", Params.tb_sl, !Params.tb_sl); - `I ("tb_el", Params.tb_el, !Params.tb_el); - `B ("cleanfp", Params.cleanfp, !Params.cleanfp); - `SO ("fpf_in", Params.fpf_in, !Params.fpf_in); - `SO ("fpf_out", Params.fpf_out, !Params.fpf_out); - `B ("fp_loaded", Params.fp_loaded, !Params.fp_loaded); - `B ("summary", Params.summary, !Params.summary); - `B ("stats", Params.stats, !Params.stats); - `B ("keep_going", Params.keep_going, !Params.keep_going); - `B ("suppress_all", Params.suppress_all, !Params.suppress_all); - `F ("timeout_stretch", Params.timeout_stretch, !Params.timeout_stretch); - `F ("backend_timeout", Params.backend_timeout, !Params.backend_timeout); -] - -let default_setting_values = setting_values () - -let setting_value_changed = - (fun (setting : setting_value) -> - match setting with - | `B (_, rf, v) -> not (!rf = v) - | `I (_, rf, v) -> not (!rf = v) - | `F (_, rf, v) -> not (!rf = v) - | `S (_, rf, v) -> not (!rf = v) - | `SO (_, rf, v) -> not (!rf = v) - ) - -let set_setting_value = - (fun (setting : setting_value) -> - match setting with - | `B (_, rf, v) -> rf := v - | `I (_, rf, v) -> rf := v - | `F (_, rf, v) -> rf := v - | `S (_, rf, v) -> rf := v - | `SO (_, rf, v) -> rf := v - ) - -let reset_setting_values () = List.iter set_setting_value default_setting_values - -let changed_setting_values () = List.filter setting_value_changed default_setting_values - -let%test "basic" = - reset_setting_values (); - init "tlapm" [|"tlapm"; "Test.tla";|] = ["Test.tla"] - && changed_setting_values () = [] - -let%test "verbose_short" = - reset_setting_values (); - init "tlapm" [|"tlapm"; "-v"; "Test.tla";|] = ["Test.tla"] - && changed_setting_values () = [`B ("verbose", Params.verbose, false)] - -let%test "verbose_long" = - reset_setting_values (); - init "tlapm" [|"tlapm"; "--verbose"; "Test.tla";|] = ["Test.tla"] - && changed_setting_values () = [`B ("verbose", Params.verbose, false)] - diff --git a/test/cli/cli_tests.ml b/test/cli/cli_tests.ml new file mode 100644 index 000000000..b07add330 --- /dev/null +++ b/test/cli/cli_tests.ml @@ -0,0 +1,134 @@ +(** Unit tests to ensure CLI parameter format does not change. +*) + +type setting_value = [ + `B of string * bool ref * bool + | `I of string * int ref * int + | `F of string * float ref * float + | `S of string * string ref * string + | `SO of string * string option ref * string option +] + +let display_setting_value (v : setting_value) : string = + match v with + | `B (n, rf, v) -> Printf.sprintf "%s: %b [%b]" n v !rf + | `I (n, rf, v) -> Printf.sprintf "%s: %d [%d]" n v !rf + | `F (n, rf, v) -> Printf.sprintf "%s: %f [%f]" n v !rf + | `S (n, rf, v) -> Printf.sprintf "%s: %s [%s]" n v !rf + | `SO (n, rf, v) -> Printf.sprintf "%s: %s [%s]" n (Option.value ~default:"None" v) (Option.value ~default:"None" !rf) + +let print_setting_diff (formatter : Format.formatter) ((expected, actual) : setting_value * setting_value) : unit = + if not (expected = actual) then ( + Printf.sprintf "exp/act: (%s)/(%s)" (display_setting_value expected) (display_setting_value actual) + |> Format.pp_print_text formatter; + ) else () + +let rec print_setting_list_diff (formatter : Format.formatter) ((expected, actual) : setting_value list * setting_value list) : unit = + match expected, actual with + | [], [] -> () + | ex :: ex_tl, [] -> + ex |> display_setting_value |> Printf.sprintf "+exp: %s" |> Format.pp_print_text formatter; + print_setting_list_diff formatter (ex_tl, []); + | [], ac :: ac_tl -> + ac |> display_setting_value |> Printf.sprintf "+act: %s" |> Format.pp_print_text formatter; + print_setting_list_diff formatter (ac_tl, []); + | ex :: ex_tl, ac :: ac_tl -> + print_setting_diff formatter (ex, ac); + print_setting_list_diff formatter (ex_tl, ac_tl) + +let setting_value_changed (setting : setting_value) = + match setting with + | `B (_, rf, v) -> not (!rf = v) + | `I (_, rf, v) -> not (!rf = v) + | `F (_, rf, v) -> not (!rf = v) + | `S (_, rf, v) -> not (!rf = v) + | `SO (_, rf, v) -> not (!rf = v) + +let changed_setting_value (setting : setting_value) = + if setting_value_changed setting then + match setting with + | `B (n, rf, _) -> Some (`B (n, rf, !rf)) + | `I (n, rf, _) -> Some (`I (n, rf, !rf)) + | `F (n, rf, _) -> Some (`F (n, rf, !rf)) + | `S (n, rf, _) -> Some (`S (n, rf, !rf)) + | `SO (n, rf, _) -> Some (`SO (n, rf, !rf)) + else None + +let set_setting_value (setting : setting_value) = + match setting with + | `B (_, rf, v) -> rf := v + | `I (_, rf, v) -> rf := v + | `F (_, rf, v) -> rf := v + | `S (_, rf, v) -> rf := v + | `SO (_, rf, v) -> rf := v + +open Tlapm_lib__Params;; + +let setting_values () : setting_value list = [ + `B ("toolbox", toolbox, !toolbox); + `I ("toolbox_vsn", toolbox_vsn, !toolbox_vsn); + `B ("use_stdin", use_stdin, !use_stdin); + `B ("prefer_stdlib", prefer_stdlib, !prefer_stdlib); + `B ("notl", notl, !notl); + `B ("verbose", verbose, !verbose); + `B ("check", check, !check); + `S ("output_dir", output_dir, !output_dir); + `I ("wait", wait, !wait); + `B ("no_fp", no_fp, !no_fp); + `I ("nofp_sl", nofp_sl, !nofp_sl); + `I ("nofp_el", nofp_el, !nofp_el); + `B ("printallobs", printallobs, !printallobs); + `B ("pr_normal", pr_normal, !pr_normal); + `B ("ob_flatten", ob_flatten, !ob_flatten); + `B ("noproving", noproving, !noproving); + `S ("fp_hist_dir", fp_hist_dir, !fp_hist_dir); + `I ("fp_original_number", fp_original_number, !fp_original_number); + `B ("safefp", safefp, !safefp); + `B ("fp_deb", fp_deb, !fp_deb); + `B ("use_xtla", use_xtla, !use_xtla); + `B ("xtla", xtla, !xtla); + `I ("tb_sl", tb_sl, !tb_sl); + `I ("tb_el", tb_el, !tb_el); + `B ("cleanfp", cleanfp, !cleanfp); + `SO ("fpf_in", fpf_in, !fpf_in); + `SO ("fpf_out", fpf_out, !fpf_out); + `B ("fp_loaded", fp_loaded, !fp_loaded); + `B ("summary", summary, !summary); + `B ("stats", stats, !stats); + `B ("keep_going", keep_going, !keep_going); + `B ("suppress_all", suppress_all, !suppress_all); + `F ("timeout_stretch", timeout_stretch, !timeout_stretch); + `F ("backend_timeout", backend_timeout, !backend_timeout); +] + +let default_setting_values = setting_values () + +let reset_setting_values () = List.iter set_setting_value default_setting_values + +let changed_setting_values () = List.filter_map changed_setting_value default_setting_values + +open OUnit2;; +open Tlapm_lib__Tlapm_args;; + +let test_basic _test_ctxt = + reset_setting_values (); + assert_equal ["Test.tla"] (init "tlapm" [|"tlapm"; "Test.tla";|]); + assert_equal [] (changed_setting_values ()) ~pp_diff:print_setting_list_diff;; + +let test_verbose_short _test_ctxt = + reset_setting_values (); + assert_equal ["Test.tla"] (init "tlapm" [|"tlapm"; "-v"; "Test.tla";|]); + assert_equal [`B ("verbose", verbose, false)] (changed_setting_values ()) ~pp_diff:print_setting_list_diff;; + +let test_verbose_long _test_ctxt = + reset_setting_values (); + assert_equal ["Test.tla"] (init "tlapm" [|"tlapm"; "--verbose"; "Test.tla";|]); + assert_equal [`B ("verbose", verbose, false)] (changed_setting_values ()) ~pp_diff:print_setting_list_diff;; + +let cli_test_suite = "Test CLI Parsing" >::: [ + "Basic Test" >:: test_basic; + "Verbose Short" >:: test_verbose_short; + "Verbose Long" >:: test_verbose_long; +];; + +let () = run_test_tt_main cli_test_suite diff --git a/test/cli/dune b/test/cli/dune new file mode 100644 index 000000000..4c31849eb --- /dev/null +++ b/test/cli/dune @@ -0,0 +1,5 @@ +(test + (name cli_tests) + (modes exe) + (libraries tlapm_lib ounit2) +) From 6a1ffb01bcea80d95dea80f27c255b925f467384 Mon Sep 17 00:00:00 2001 From: Andrew Helwer Date: Wed, 22 Oct 2025 12:26:24 -0700 Subject: [PATCH 03/11] Record output and trap calls to exit Signed-off-by: Andrew Helwer --- src/tlapm_args.ml | 14 +++++----- src/tlapm_args.mli | 2 +- src/tlapm_lib.ml | 4 +-- test/cli/cli_tests.ml | 59 +++++++++++++++++++++++++++++++++++++------ 4 files changed, 61 insertions(+), 18 deletions(-) diff --git a/src/tlapm_args.ml b/src/tlapm_args.ml index d4e66dabb..9670d0598 100644 --- a/src/tlapm_args.ml +++ b/src/tlapm_args.ml @@ -135,7 +135,7 @@ let quote_if_needed s = end -let init (executable_name : string) (args : string array) = +let init (executable_name : string) (args : string array) (err : Format.formatter) (terminate : int -> unit) = let mods = ref [] in let helpfn = ref (fun () -> ()) in let show_help () = !helpfn () in @@ -246,22 +246,22 @@ let init (executable_name : string) (args : string array) = format_of_string "Usage: %s FILE ...\noptions are:" in helpfn := begin fun () -> - Arg.usage opts - (Printf.sprintf usage_fmt (Filename.basename executable_name)) ; - exit 0 + Format.pp_print_text err (Arg.usage_string opts + (Printf.sprintf usage_fmt (Filename.basename executable_name))); + terminate 0 end ; parse_args executable_name args opts mods usage_fmt ; if !show_config || !verbose then begin (*print_endline (printconfig true) ;*) flush stdout end ; - if !show_config then exit 0 ; + if !show_config then terminate 0 ; if !mods = [] then begin Arg.usage opts (Printf.sprintf "Need at least one module file.\n\n\ Usage: %s FILE ...\noptions are:" (Filename.basename executable_name)) ; - exit 2 + terminate 2 end ; if !summary then begin suppress_all := true ; @@ -283,6 +283,6 @@ let init (executable_name : string) (args : string array) = Arg.usage opts "Exactly 1 module has to be specified if TLAPM is invoked with\ the --stdin option." ; - exit 2 + terminate 2 end; !mods diff --git a/src/tlapm_args.mli b/src/tlapm_args.mli index ec5c92751..441cf0c98 100644 --- a/src/tlapm_args.mli +++ b/src/tlapm_args.mli @@ -8,4 +8,4 @@ Copyright (C) 2011 INRIA and Microsoft Corporation or directly takes action such as printing out file contents or deleting directories. Returns a list of files for proof checking. *) -val init: string -> string array -> string list +val init: string -> string array -> Format.formatter -> (int -> unit) -> string list diff --git a/src/tlapm_lib.ml b/src/tlapm_lib.ml index 4bd57a162..dddc31789 100644 --- a/src/tlapm_lib.ml +++ b/src/tlapm_lib.ml @@ -586,9 +586,9 @@ let init () = Printexc.record_backtrace true; Format.pp_set_max_indent Format.err_formatter 35; if Params.debugging "main" then - main (Tlapm_args.init Sys.executable_name Sys.argv) + main (Tlapm_args.init Sys.executable_name Sys.argv Format.err_formatter exit) else - try main (Tlapm_args.init Sys.executable_name Sys.argv) with + try main (Tlapm_args.init Sys.executable_name Sys.argv Format.err_formatter exit) with | Errors.Fatal -> Util.eprintf "tlapm: Exiting because of the above error."; exit 0; diff --git a/test/cli/cli_tests.ml b/test/cli/cli_tests.ml index b07add330..bd5bb6008 100644 --- a/test/cli/cli_tests.ml +++ b/test/cli/cli_tests.ml @@ -107,28 +107,71 @@ let reset_setting_values () = List.iter set_setting_value default_setting_values let changed_setting_values () = List.filter_map changed_setting_value default_setting_values +let parse_args (args : string list) : string list * string * int option = + let buffer = Buffer.create 0 in + let exception TrappedExit of int in + let terminate (code : int) = raise (TrappedExit code) in + try let mods = Tlapm_lib__Tlapm_args.init "tlapm" (Array.of_list ("tlapm" :: args)) (Format.formatter_of_buffer buffer) terminate in + (mods, Buffer.contents buffer, None) + with TrappedExit exit_code -> ([], Buffer.contents buffer, Some exit_code) + open OUnit2;; -open Tlapm_lib__Tlapm_args;; + +let test_help _test_ctxt = + reset_setting_values (); + let (mods, output, exit_code) = parse_args ["--help"] in + assert_equal [] mods; + assert_bool "Should print help text" (String.starts_with output ~prefix:"Usage: tlapm FILE"); + assert_equal (Some 0) exit_code; + assert_equal [] (changed_setting_values ()) ~pp_diff:print_setting_list_diff;; let test_basic _test_ctxt = reset_setting_values (); - assert_equal ["Test.tla"] (init "tlapm" [|"tlapm"; "Test.tla";|]); + let (mods, output, exit_code) = parse_args ["Test.tla"] in + assert_equal ["Test.tla"] mods; + assert_equal "" output; + assert_equal None exit_code; assert_equal [] (changed_setting_values ()) ~pp_diff:print_setting_list_diff;; let test_verbose_short _test_ctxt = reset_setting_values (); - assert_equal ["Test.tla"] (init "tlapm" [|"tlapm"; "-v"; "Test.tla";|]); - assert_equal [`B ("verbose", verbose, false)] (changed_setting_values ()) ~pp_diff:print_setting_list_diff;; + let (mods, output, exit_code) = parse_args ["-v"; "Test.tla"] in + assert_equal ["Test.tla"] mods; + assert_equal "" output; + assert_equal None exit_code; + assert_equal [`B ("verbose", verbose, true)] (changed_setting_values ()) ~pp_diff:print_setting_list_diff;; let test_verbose_long _test_ctxt = reset_setting_values (); - assert_equal ["Test.tla"] (init "tlapm" [|"tlapm"; "--verbose"; "Test.tla";|]); - assert_equal [`B ("verbose", verbose, false)] (changed_setting_values ()) ~pp_diff:print_setting_list_diff;; + let (mods, output, exit_code) = parse_args ["--verbose"; "Test.tla"] in + assert_equal ["Test.tla"] mods; + assert_equal "" output; + assert_equal None exit_code; + assert_equal [`B ("verbose", verbose, true)] (changed_setting_values ()) ~pp_diff:print_setting_list_diff;; + +let test_use_stdin _test_ctxt = + reset_setting_values (); + let (mods, output, exit_code) = parse_args ["--stdin"; "Test.tla"] in + assert_equal ["Test.tla"] mods; + assert_equal "" output; + assert_equal None exit_code; + assert_equal [`B ("use_stdin", use_stdin, true)] (changed_setting_values ()) ~pp_diff:print_setting_list_diff;; + +let test_prefer_stdlib _test_ctxt = + reset_setting_values (); + let (mods, output, exit_code) = parse_args ["--prefer-stdlib"; "Test.tla"] in + assert_equal ["Test.tla"] mods; + assert_equal "" output; + assert_equal None exit_code; + assert_equal [`B ("prefer_stdlib", prefer_stdlib, true)] (changed_setting_values ()) ~pp_diff:print_setting_list_diff;; let cli_test_suite = "Test CLI Parsing" >::: [ - "Basic Test" >:: test_basic; + "Help Test" >:: test_help; + "Basic Test" >:: test_basic; "Verbose Short" >:: test_verbose_short; - "Verbose Long" >:: test_verbose_long; + "Verbose Long" >:: test_verbose_long; + "Use Stdin" >:: test_use_stdin; + "Prefer Stdlib" >:: test_prefer_stdlib; ];; let () = run_test_tt_main cli_test_suite From c67672acd87c427dc820cb3e518a9e794d4c39df Mon Sep 17 00:00:00 2001 From: Andrew Helwer Date: Thu, 23 Oct 2025 13:46:20 -0700 Subject: [PATCH 04/11] Add test for version flag Signed-off-by: Andrew Helwer --- src/tlapm_args.ml | 20 +++++------ src/tlapm_args.mli | 2 +- src/tlapm_lib.ml | 4 +-- test/cli/cli_tests.ml | 84 ++++++++++++++++++++++++++++++------------- 4 files changed, 73 insertions(+), 37 deletions(-) diff --git a/src/tlapm_args.ml b/src/tlapm_args.ml index 9670d0598..9e1db3e3a 100644 --- a/src/tlapm_args.ml +++ b/src/tlapm_args.ml @@ -7,10 +7,10 @@ open Params let show_config = ref false -let show_version () = - print_endline (rawversion ()) ; - exit 0 - +let show_version formatter terminate = + Format.pp_print_text formatter (rawversion ()); + Format.pp_print_cut formatter (); + terminate 0 let set_debug_flags flgs = let flgs = Ext.split flgs ',' in @@ -135,7 +135,7 @@ let quote_if_needed s = end -let init (executable_name : string) (args : string array) (err : Format.formatter) (terminate : int -> unit) = +let init ?(out=Format.std_formatter) ?(err=Format.err_formatter) ?(terminate=exit) (executable_name : string) (args : string array) = let mods = ref [] in let helpfn = ref (fun () -> ()) in let show_help () = !helpfn () in @@ -148,7 +148,7 @@ let init (executable_name : string) (args : string array) (err : Format.formatte blank; "--help", Arg.Unit show_help, " show this help message and exit" ; "-help", Arg.Unit show_help, " (same as --help)" ; - "--version", Arg.Unit show_version, " show version number and exit" ; + "--version", Arg.Unit (fun () -> show_version out terminate), " show version number and exit" ; "--verbose", Arg.Set verbose, " produce verbose messages" ; "-v", Arg.Set verbose, " (same as --verbose)" ; blank; @@ -252,15 +252,15 @@ let init (executable_name : string) (args : string array) (err : Format.formatte end ; parse_args executable_name args opts mods usage_fmt ; if !show_config || !verbose then begin - (*print_endline (printconfig true) ;*) - flush stdout + Format.pp_print_text out (printconfig true); + Format.pp_print_cut out (); end ; if !show_config then terminate 0 ; if !mods = [] then begin - Arg.usage opts + Format.pp_print_text err (Arg.usage_string opts (Printf.sprintf "Need at least one module file.\n\n\ Usage: %s FILE ...\noptions are:" - (Filename.basename executable_name)) ; + (Filename.basename executable_name))); terminate 2 end ; if !summary then begin diff --git a/src/tlapm_args.mli b/src/tlapm_args.mli index 441cf0c98..6bde11eef 100644 --- a/src/tlapm_args.mli +++ b/src/tlapm_args.mli @@ -8,4 +8,4 @@ Copyright (C) 2011 INRIA and Microsoft Corporation or directly takes action such as printing out file contents or deleting directories. Returns a list of files for proof checking. *) -val init: string -> string array -> Format.formatter -> (int -> unit) -> string list +val init: ?out:Format.formatter -> ?err:Format.formatter -> ?terminate:(int -> unit) -> string -> string array -> string list diff --git a/src/tlapm_lib.ml b/src/tlapm_lib.ml index dddc31789..4bd57a162 100644 --- a/src/tlapm_lib.ml +++ b/src/tlapm_lib.ml @@ -586,9 +586,9 @@ let init () = Printexc.record_backtrace true; Format.pp_set_max_indent Format.err_formatter 35; if Params.debugging "main" then - main (Tlapm_args.init Sys.executable_name Sys.argv Format.err_formatter exit) + main (Tlapm_args.init Sys.executable_name Sys.argv) else - try main (Tlapm_args.init Sys.executable_name Sys.argv Format.err_formatter exit) with + try main (Tlapm_args.init Sys.executable_name Sys.argv) with | Errors.Fatal -> Util.eprintf "tlapm: Exiting because of the above error."; exit 0; diff --git a/test/cli/cli_tests.ml b/test/cli/cli_tests.ml index bd5bb6008..764d4ec77 100644 --- a/test/cli/cli_tests.ml +++ b/test/cli/cli_tests.ml @@ -107,71 +107,107 @@ let reset_setting_values () = List.iter set_setting_value default_setting_values let changed_setting_values () = List.filter_map changed_setting_value default_setting_values -let parse_args (args : string list) : string list * string * int option = - let buffer = Buffer.create 0 in +let parse_args (args : string list) : string list * string * string * int option = + let out = Buffer.create 0 in + let out_format = Format.formatter_of_buffer out in + let err = Buffer.create 0 in + let err_format = Format.formatter_of_buffer err in let exception TrappedExit of int in let terminate (code : int) = raise (TrappedExit code) in - try let mods = Tlapm_lib__Tlapm_args.init "tlapm" (Array.of_list ("tlapm" :: args)) (Format.formatter_of_buffer buffer) terminate in - (mods, Buffer.contents buffer, None) - with TrappedExit exit_code -> ([], Buffer.contents buffer, Some exit_code) + try let mods = Tlapm_lib__Tlapm_args.init ~out:out_format ~err:err_format ~terminate:terminate "tlapm" (Array.of_list ("tlapm" :: args)) in + Format.pp_print_flush out_format (); + Format.pp_print_flush err_format (); + (mods, Buffer.contents out, Buffer.contents err, None) + with TrappedExit exit_code -> + Format.pp_print_flush out_format (); + Format.pp_print_flush err_format (); + ([], Buffer.contents out, Buffer.contents err, Some exit_code) open OUnit2;; let test_help _test_ctxt = reset_setting_values (); - let (mods, output, exit_code) = parse_args ["--help"] in + let (mods, out, err, exit_code) = parse_args ["--help"] in assert_equal [] mods; - assert_bool "Should print help text" (String.starts_with output ~prefix:"Usage: tlapm FILE"); + assert_equal "" out; + assert_bool "Should print help text" (String.starts_with err ~prefix:"Usage: tlapm FILE"); + assert_equal (Some 0) exit_code; + let (mods, out, err, exit_code) = parse_args ["-help"] in + assert_equal [] mods; + assert_equal "" out; + assert_bool "Should print help text" (String.starts_with err ~prefix:"Usage: tlapm FILE"); + assert_equal (Some 0) exit_code; + assert_equal [] (changed_setting_values ()) ~pp_diff:print_setting_list_diff;; + +let test_version _test_ctxt = + reset_setting_values (); + let (mods, out, err, exit_code) = parse_args ["--version"] in + assert_equal [] mods; + assert_equal (rawversion () ^ "\n") out; + assert_equal "" err; assert_equal (Some 0) exit_code; assert_equal [] (changed_setting_values ()) ~pp_diff:print_setting_list_diff;; let test_basic _test_ctxt = reset_setting_values (); - let (mods, output, exit_code) = parse_args ["Test.tla"] in + let (mods, out, err, exit_code) = parse_args ["Test.tla"] in assert_equal ["Test.tla"] mods; - assert_equal "" output; + assert_equal "" out; + assert_equal "" err; assert_equal None exit_code; assert_equal [] (changed_setting_values ()) ~pp_diff:print_setting_list_diff;; -let test_verbose_short _test_ctxt = +let test_no_mods _test_ctxt = + reset_setting_values (); + let (mods, out, err, exit_code) = parse_args [] in + assert_equal [] mods; + assert_equal "" out; + assert_bool "Need module req message" (String.starts_with err ~prefix:"Need at least one module file"); + assert_equal (Some 2) exit_code; + assert_equal [] (changed_setting_values ()) ~pp_diff:print_setting_list_diff;; + +let test_verbose _test_ctxt = reset_setting_values (); - let (mods, output, exit_code) = parse_args ["-v"; "Test.tla"] in + let (mods, out, err, exit_code) = parse_args ["-v"; "Test.tla"] in assert_equal ["Test.tla"] mods; - assert_equal "" output; + assert_bool "Need config" (String.starts_with out ~prefix:"-------------------- tlapm configuration --------------------"); + assert_equal "" err; assert_equal None exit_code; assert_equal [`B ("verbose", verbose, true)] (changed_setting_values ()) ~pp_diff:print_setting_list_diff;; - -let test_verbose_long _test_ctxt = reset_setting_values (); - let (mods, output, exit_code) = parse_args ["--verbose"; "Test.tla"] in + let (mods, out, err, exit_code) = parse_args ["--verbose"; "Test.tla"] in assert_equal ["Test.tla"] mods; - assert_equal "" output; + assert_bool "Need config" (String.starts_with out ~prefix:"-------------------- tlapm configuration --------------------"); + assert_equal "" err; assert_equal None exit_code; assert_equal [`B ("verbose", verbose, true)] (changed_setting_values ()) ~pp_diff:print_setting_list_diff;; let test_use_stdin _test_ctxt = reset_setting_values (); - let (mods, output, exit_code) = parse_args ["--stdin"; "Test.tla"] in + let (mods, out, err, exit_code) = parse_args ["--stdin"; "Test.tla"] in assert_equal ["Test.tla"] mods; - assert_equal "" output; + assert_equal "" out; + assert_equal "" err; assert_equal None exit_code; assert_equal [`B ("use_stdin", use_stdin, true)] (changed_setting_values ()) ~pp_diff:print_setting_list_diff;; let test_prefer_stdlib _test_ctxt = reset_setting_values (); - let (mods, output, exit_code) = parse_args ["--prefer-stdlib"; "Test.tla"] in + let (mods, out, err, exit_code) = parse_args ["--prefer-stdlib"; "Test.tla"] in assert_equal ["Test.tla"] mods; - assert_equal "" output; + assert_equal "" out; + assert_equal "" err; assert_equal None exit_code; assert_equal [`B ("prefer_stdlib", prefer_stdlib, true)] (changed_setting_values ()) ~pp_diff:print_setting_list_diff;; let cli_test_suite = "Test CLI Parsing" >::: [ "Help Test" >:: test_help; "Basic Test" >:: test_basic; - "Verbose Short" >:: test_verbose_short; - "Verbose Long" >:: test_verbose_long; - "Use Stdin" >:: test_use_stdin; - "Prefer Stdlib" >:: test_prefer_stdlib; + "Version Test" >:: test_version; + "No Mods Test" >:: test_no_mods; + "Verbose Test" >:: test_verbose; + "Use Stdin Test" >:: test_use_stdin; + "Prefer Stdlib Test" >:: test_prefer_stdlib; ];; let () = run_test_tt_main cli_test_suite From b86448a571b0bfdc84ec1779fff003da220cf64b Mon Sep 17 00:00:00 2001 From: Andrew Helwer Date: Mon, 24 Nov 2025 15:00:50 -0800 Subject: [PATCH 05/11] Swallow error dumped to stderr Signed-off-by: Andrew Helwer --- src/params.ml | 26 ++++++++++++------------ src/params.mli | 4 ++-- src/tlapm_args.ml | 47 ++++++++++++++++++++++--------------------- src/util/util.ml | 2 +- test/cli/cli_tests.ml | 15 ++++++++++++-- 5 files changed, 53 insertions(+), 41 deletions(-) diff --git a/src/params.ml b/src/params.ml index 5ad2fbbd3..56381cbd4 100644 --- a/src/params.ml +++ b/src/params.ml @@ -102,7 +102,7 @@ type exec = executable ref let path_prefix = sprintf "PATH='%s';" Paths.backend_path_string -let get_exec e = +let get_exec err e = match !e with | Unchecked (exec, cmd, vers) -> (* @@ -131,7 +131,7 @@ let get_exec e = else "." in let msg = msg1 ^ msg2 in - eprintf "%s" msg; + Format.pp_print_text err msg; e := NotFound msg; failwith msg; end; @@ -450,14 +450,14 @@ let stats = ref false let solve_cmd cmd file = if Sys.os_type = "Cygwin" then - sprintf "file=%s; winfile=\"`cygpath -a -w \"%s\"`\"; %s" file file (get_exec cmd) + sprintf "file=%s; winfile=\"`cygpath -a -w \"%s\"`\"; %s" file file (get_exec Format.err_formatter cmd) else - sprintf "file=%s; %s" file (get_exec cmd) + sprintf "file=%s; %s" file (get_exec Format.err_formatter cmd) -let external_tool_config force (name, tool) = +let external_tool_config (err : Format.formatter) force (name, tool) = if force then begin - try ignore (get_exec tool) with Failure _ -> () + try ignore (get_exec err tool) with Failure _ -> () end; match !tool with | Checked (cmd, []) -> @@ -470,7 +470,7 @@ let external_tool_config force (name, tool) = | _ -> [] -let configuration toolbox force = +let configuration err toolbox force = let library_path = (match stdlib_path with | Some path -> "\"" ^ (String.escaped path) ^ "\""; | None -> "N/A") @@ -494,7 +494,7 @@ let configuration toolbox force = first_line :: mid_lines @ [last_line] end end - @ List.flatten (List.map (external_tool_config force) + @ List.flatten (List.map (external_tool_config err force) [("Isabelle", isabelle); ("zenon", zenon); ("CVC4", cvc4); @@ -517,17 +517,17 @@ let configuration toolbox force = header @ lines @ footer -let printconfig force = - String.concat "\n" (configuration false force) +let printconfig err force = + String.concat "\n" (configuration err false force) let print_config_toolbox force = - String.concat "\n" (configuration true force) + String.concat "\n" (configuration Format.err_formatter true force) let zenon_version = ref None let check_zenon_ver () = - let zen = get_exec zenon in + let zen = get_exec Format.err_formatter zenon in match get_version zenon with | [] -> () | ret :: _ -> @@ -543,7 +543,7 @@ let get_zenon_verfp () = if !zenon_version = None then check_zenon_ver (); let isabelle_version = ref None let check_isabelle_ver () = - (try ignore (get_exec isabelle) with Failure _ -> ()); + (try ignore (get_exec Format.err_formatter isabelle) with Failure _ -> ()); match get_version isabelle with | [] -> () | ret :: _ -> diff --git a/src/params.mli b/src/params.mli index 52592cd3f..adf1ed3e5 100644 --- a/src/params.mli +++ b/src/params.mli @@ -66,7 +66,7 @@ val safefp: bool ref val fp_deb: bool ref (* util/util.ml *) -val configuration: bool -> bool -> string list +val configuration: Format.formatter -> bool -> bool -> string list (* module/save.ml *) val stdlib_search_paths : string list @@ -97,7 +97,7 @@ val suppress_all: bool ref val set_smt_logic: string -> unit val set_smt_solver: string -> unit val set_tlapm_cache_dir: string -> unit -val printconfig: bool -> string +val printconfig: Format.formatter -> bool -> string val print_config_toolbox: bool -> string val check_zenon_ver: unit -> unit val fpf_out: string option ref diff --git a/src/tlapm_args.ml b/src/tlapm_args.ml index 9e1db3e3a..c3b0f80de 100644 --- a/src/tlapm_args.ml +++ b/src/tlapm_args.ml @@ -53,24 +53,23 @@ let set_default_method meth = (* FIXME use Arg.parse instead *) -let parse_args executable_name args opts mods usage_fmt = +let parse_args executable_name args opts mods usage_fmt err terminate = try Arg.current := 0; Arg.parse_argv args opts (fun mfile -> mods := mfile :: !mods) (Printf.sprintf usage_fmt (Filename.basename executable_name)) with Arg.Bad msg -> - print_endline msg ; - flush stdout ; - exit 2 + Format.pp_print_text err msg; + terminate 2 -let show_where () = +let show_where out terminate = match stdlib_path with | Some path -> - Printf.printf "%s\n" path; - exit 0 + Printf.sprintf "%s\n" path |> Format.pp_print_text out; + terminate 0 | None -> - Printf.printf "N/A\n"; - exit 1 + Format.pp_print_text out "N/A\n"; + terminate 1 let set_nofp_start s = nofp_sl := s @@ -152,7 +151,7 @@ let init ?(out=Format.std_formatter) ?(err=Format.err_formatter) ?(terminate=exi "--verbose", Arg.Set verbose, " produce verbose messages" ; "-v", Arg.Set verbose, " (same as --verbose)" ; blank; - "--where", Arg.Unit show_where, + "--where", Arg.Unit (fun () -> show_where out terminate), " show location of standard library and exit" ; "--config", Arg.Set show_config, " show configuration and exit" ; "--summary", Arg.Set summary, @@ -246,21 +245,21 @@ let init ?(out=Format.std_formatter) ?(err=Format.err_formatter) ?(terminate=exi format_of_string "Usage: %s FILE ...\noptions are:" in helpfn := begin fun () -> - Format.pp_print_text err (Arg.usage_string opts - (Printf.sprintf usage_fmt (Filename.basename executable_name))); + Arg.usage_string opts + (Printf.sprintf usage_fmt (Filename.basename executable_name)) |> Format.pp_print_text err; terminate 0 end ; - parse_args executable_name args opts mods usage_fmt ; + parse_args executable_name args opts mods usage_fmt err terminate; if !show_config || !verbose then begin - Format.pp_print_text out (printconfig true); + Format.pp_print_text out (printconfig err true); Format.pp_print_cut out (); end ; if !show_config then terminate 0 ; if !mods = [] then begin - Format.pp_print_text err (Arg.usage_string opts + Arg.usage_string opts (Printf.sprintf "Need at least one module file.\n\n\ Usage: %s FILE ...\noptions are:" - (Filename.basename executable_name))); + (Filename.basename executable_name)) |> Format.pp_print_text err; terminate 2 end ; if !summary then begin @@ -269,15 +268,17 @@ let init ?(out=Format.std_formatter) ?(err=Format.err_formatter) ?(terminate=exi end ; check_zenon_ver () ; if !Params.toolbox then begin - Printf.printf "\n\\* TLAPM version %s\n" - (Params.rawversion ()); + Printf.sprintf "\n\\* TLAPM version %s\n" + (Params.rawversion ()) + |> Format.pp_print_text out; let tm = Unix.localtime (Unix.gettimeofday ()) in - Printf.printf "\\* launched at %04d-%02d-%02d %02d:%02d:%02d" + Printf.sprintf "\\* launched at %04d-%02d-%02d %02d:%02d:%02d" (tm.Unix.tm_year + 1900) (tm.Unix.tm_mon + 1) tm.Unix.tm_mday - tm.Unix.tm_hour tm.Unix.tm_min tm.Unix.tm_sec; - Printf.printf " with command line:\n\\*"; - Array.iter (fun s -> Printf.printf " %s" (quote_if_needed s)) args; - Printf.printf "\n\n%!" + tm.Unix.tm_hour tm.Unix.tm_min tm.Unix.tm_sec + |> Format.pp_print_text out; + Printf.sprintf " with command line:\n\\*" |> Format.pp_print_text out; + Array.iter (fun s -> Printf.sprintf " %s" (quote_if_needed s) |> Format.pp_print_text out) args; + Format.pp_print_text out "\n\n%!" end; if !use_stdin && (List.length !mods) <> 1 then begin Arg.usage opts diff --git a/src/util/util.ml b/src/util/util.ml index 6f7096bfb..b91c13ab0 100644 --- a/src/util/util.ml +++ b/src/util/util.ml @@ -117,7 +117,7 @@ let bug ?at msg = "Please file a bug report, including as much information" ; "as you can. Mention the following in your report: " ; "" ] - @ Params.configuration false false + @ Params.configuration Format.err_formatter false false in String.concat "\n" lines ^ "\n" in diff --git a/test/cli/cli_tests.ml b/test/cli/cli_tests.ml index 764d4ec77..b26f66cd5 100644 --- a/test/cli/cli_tests.ml +++ b/test/cli/cli_tests.ml @@ -175,10 +175,10 @@ let test_verbose _test_ctxt = assert_equal None exit_code; assert_equal [`B ("verbose", verbose, true)] (changed_setting_values ()) ~pp_diff:print_setting_list_diff;; reset_setting_values (); - let (mods, out, err, exit_code) = parse_args ["--verbose"; "Test.tla"] in + let (mods, out, _err, exit_code) = parse_args ["--verbose"; "Test.tla"] in assert_equal ["Test.tla"] mods; assert_bool "Need config" (String.starts_with out ~prefix:"-------------------- tlapm configuration --------------------"); - assert_equal "" err; + (* err probably has output due to being unable to find tools; ignore *) assert_equal None exit_code; assert_equal [`B ("verbose", verbose, true)] (changed_setting_values ()) ~pp_diff:print_setting_list_diff;; @@ -200,6 +200,16 @@ let test_prefer_stdlib _test_ctxt = assert_equal None exit_code; assert_equal [`B ("prefer_stdlib", prefer_stdlib, true)] (changed_setting_values ()) ~pp_diff:print_setting_list_diff;; + +let test_where _test_ctxt = + reset_setting_values (); + let (mods, out, err, exit_code) = parse_args ["--where"; "Test.tla"] in + assert_equal [] mods; + assert_bool "Need stlib path" (not (String.equal out "")); + assert_equal "" err; + assert_equal (Some 0) exit_code; + assert_equal [] (changed_setting_values ()) ~pp_diff:print_setting_list_diff;; + let cli_test_suite = "Test CLI Parsing" >::: [ "Help Test" >:: test_help; "Basic Test" >:: test_basic; @@ -208,6 +218,7 @@ let cli_test_suite = "Test CLI Parsing" >::: [ "Verbose Test" >:: test_verbose; "Use Stdin Test" >:: test_use_stdin; "Prefer Stdlib Test" >:: test_prefer_stdlib; + "Print Stlib Location Test" >:: test_where; ];; let () = run_test_tt_main cli_test_suite From 295216cfbdd43e89c302dfca55b77a22abe8db12 Mon Sep 17 00:00:00 2001 From: Andrew Helwer Date: Mon, 24 Nov 2025 17:20:16 -0800 Subject: [PATCH 06/11] Added tests for some more options Signed-off-by: Andrew Helwer --- test/cli/cli_tests.ml | 42 +++++++++++++++++++++++++++++++----------- 1 file changed, 31 insertions(+), 11 deletions(-) diff --git a/test/cli/cli_tests.ml b/test/cli/cli_tests.ml index b26f66cd5..63061e875 100644 --- a/test/cli/cli_tests.ml +++ b/test/cli/cli_tests.ml @@ -182,6 +182,34 @@ let test_verbose _test_ctxt = assert_equal None exit_code; assert_equal [`B ("verbose", verbose, true)] (changed_setting_values ()) ~pp_diff:print_setting_list_diff;; +let test_where _test_ctxt = + reset_setting_values (); + let (mods, out, err, exit_code) = parse_args ["--where"] in + assert_equal [] mods; + assert_bool "Need stlib path" (not (String.equal out "")); + assert_equal "" err; + assert_equal (Some 0) exit_code; + assert_equal [] (changed_setting_values ()) ~pp_diff:print_setting_list_diff;; + +let test_config _test_ctxt = + reset_setting_values (); + let (mods, out, _err, exit_code) = parse_args ["--config"] in + assert_equal [] mods; + assert_bool "Need config" (String.starts_with out ~prefix:"-------------------- tlapm configuration --------------------"); + (* err probably has output due to being unable to find tools; ignore *) + assert_equal (Some 0) exit_code; + assert_equal [] (changed_setting_values ()) ~pp_diff:print_setting_list_diff;; + +let test_summary _test_ctxt = + reset_setting_values (); + let (mods, out, err, exit_code) = parse_args ["--summary"; "Test.tla"] in + assert_equal ["Test.tla"] mods; + assert_equal "" out; + assert_equal "" err; + assert_equal None exit_code; + assert_equal [`B ("summary", summary, true); `B ("suppress_all", suppress_all, true)] (changed_setting_values ()) ~pp_diff:print_setting_list_diff; + assert_equal false !check;; + let test_use_stdin _test_ctxt = reset_setting_values (); let (mods, out, err, exit_code) = parse_args ["--stdin"; "Test.tla"] in @@ -200,25 +228,17 @@ let test_prefer_stdlib _test_ctxt = assert_equal None exit_code; assert_equal [`B ("prefer_stdlib", prefer_stdlib, true)] (changed_setting_values ()) ~pp_diff:print_setting_list_diff;; - -let test_where _test_ctxt = - reset_setting_values (); - let (mods, out, err, exit_code) = parse_args ["--where"; "Test.tla"] in - assert_equal [] mods; - assert_bool "Need stlib path" (not (String.equal out "")); - assert_equal "" err; - assert_equal (Some 0) exit_code; - assert_equal [] (changed_setting_values ()) ~pp_diff:print_setting_list_diff;; - let cli_test_suite = "Test CLI Parsing" >::: [ "Help Test" >:: test_help; "Basic Test" >:: test_basic; "Version Test" >:: test_version; "No Mods Test" >:: test_no_mods; "Verbose Test" >:: test_verbose; + "Print Stlib Location Test" >:: test_where; + "Print Config Test" >:: test_config; + "Print Summary Test" >:: test_summary; "Use Stdin Test" >:: test_use_stdin; "Prefer Stdlib Test" >:: test_prefer_stdlib; - "Print Stlib Location Test" >:: test_where; ];; let () = run_test_tt_main cli_test_suite From ad5871652f7812c46026105ce411c963b2fe45e8 Mon Sep 17 00:00:00 2001 From: Andrew Helwer Date: Wed, 26 Nov 2025 19:40:55 -0800 Subject: [PATCH 07/11] More tests for more options Signed-off-by: Andrew Helwer --- src/tlapm_args.ml | 2 +- test/cli/cli_tests.ml | 161 ++++++++++++++++++++++++++++++++---------- 2 files changed, 124 insertions(+), 39 deletions(-) diff --git a/src/tlapm_args.ml b/src/tlapm_args.ml index c3b0f80de..a01f5694e 100644 --- a/src/tlapm_args.ml +++ b/src/tlapm_args.ml @@ -6,7 +6,6 @@ open Ext open Params -let show_config = ref false let show_version formatter terminate = Format.pp_print_text formatter (rawversion ()); Format.pp_print_cut formatter (); @@ -135,6 +134,7 @@ let quote_if_needed s = let init ?(out=Format.std_formatter) ?(err=Format.err_formatter) ?(terminate=exit) (executable_name : string) (args : string array) = + let show_config = ref false in let mods = ref [] in let helpfn = ref (fun () -> ()) in let show_help () = !helpfn () in diff --git a/test/cli/cli_tests.ml b/test/cli/cli_tests.ml index 63061e875..eee431d36 100644 --- a/test/cli/cli_tests.ml +++ b/test/cli/cli_tests.ml @@ -7,8 +7,19 @@ type setting_value = [ | `F of string * float ref * float | `S of string * string ref * string | `SO of string * string option ref * string option + | `SL of string * string list ref * string list ] +let rec string_contains (needle : string) (haystack : string) : bool = + match haystack with + | "" -> false + | _ -> String.starts_with ~prefix:needle haystack || + String.sub haystack 1 ((String.length haystack) - 1) |> + string_contains needle + +let str_ls_as_str (ls : string list) : string = + List.fold_left (^) "[" ls + let display_setting_value (v : setting_value) : string = match v with | `B (n, rf, v) -> Printf.sprintf "%s: %b [%b]" n v !rf @@ -16,25 +27,29 @@ let display_setting_value (v : setting_value) : string = | `F (n, rf, v) -> Printf.sprintf "%s: %f [%f]" n v !rf | `S (n, rf, v) -> Printf.sprintf "%s: %s [%s]" n v !rf | `SO (n, rf, v) -> Printf.sprintf "%s: %s [%s]" n (Option.value ~default:"None" v) (Option.value ~default:"None" !rf) + | `SL (n, rf, v) -> Printf.sprintf "%s: %s [%s]" n (str_ls_as_str v) (str_ls_as_str !rf) -let print_setting_diff (formatter : Format.formatter) ((expected, actual) : setting_value * setting_value) : unit = - if not (expected = actual) then ( - Printf.sprintf "exp/act: (%s)/(%s)" (display_setting_value expected) (display_setting_value actual) - |> Format.pp_print_text formatter; - ) else () +let print_string_diff (formatter : Format.formatter) ((expected, actual) : string * string) : unit = + Printf.sprintf "exp/act: (%s)/(%s)" expected actual |> Format.pp_print_text formatter -let rec print_setting_list_diff (formatter : Format.formatter) ((expected, actual) : setting_value list * setting_value list) : unit = +let rec print_list_diff (formatter : Format.formatter) (expected : 'a list) (actual : 'a list) (as_string : 'a -> string) : unit = match expected, actual with | [], [] -> () | ex :: ex_tl, [] -> - ex |> display_setting_value |> Printf.sprintf "+exp: %s" |> Format.pp_print_text formatter; - print_setting_list_diff formatter (ex_tl, []); + ex |> as_string |> Printf.sprintf "+exp: %s" |> Format.pp_print_text formatter; + print_list_diff formatter ex_tl [] as_string; | [], ac :: ac_tl -> - ac |> display_setting_value |> Printf.sprintf "+act: %s" |> Format.pp_print_text formatter; - print_setting_list_diff formatter (ac_tl, []); + ac |> as_string |> Printf.sprintf "+act: %s" |> Format.pp_print_text formatter; + print_list_diff formatter ac_tl [] as_string; | ex :: ex_tl, ac :: ac_tl -> - print_setting_diff formatter (ex, ac); - print_setting_list_diff formatter (ex_tl, ac_tl) + if not (ex = ac) then print_string_diff formatter (as_string ex, as_string ac); + print_list_diff formatter ex_tl ac_tl as_string + +let print_setting_list_diff (formatter : Format.formatter) ((expected, actual) : setting_value list * setting_value list) : unit = + print_list_diff formatter expected actual display_setting_value + +let print_mod_diff (formatter : Format.formatter) ((expected, actual) : string list * string list) : unit = + print_list_diff formatter expected actual (fun s -> s) let setting_value_changed (setting : setting_value) = match setting with @@ -43,6 +58,7 @@ let setting_value_changed (setting : setting_value) = | `F (_, rf, v) -> not (!rf = v) | `S (_, rf, v) -> not (!rf = v) | `SO (_, rf, v) -> not (!rf = v) + | `SL (_, rf, v) -> not (List.equal String.equal !rf v) let changed_setting_value (setting : setting_value) = if setting_value_changed setting then @@ -52,6 +68,7 @@ let changed_setting_value (setting : setting_value) = | `F (n, rf, _) -> Some (`F (n, rf, !rf)) | `S (n, rf, _) -> Some (`S (n, rf, !rf)) | `SO (n, rf, _) -> Some (`SO (n, rf, !rf)) + | `SL (n, rf, _) -> Some (`SL (n, rf, !rf)) else None let set_setting_value (setting : setting_value) = @@ -61,6 +78,7 @@ let set_setting_value (setting : setting_value) = | `F (_, rf, v) -> rf := v | `S (_, rf, v) -> rf := v | `SO (_, rf, v) -> rf := v + | `SL (_, rf, v) -> rf := v open Tlapm_lib__Params;; @@ -89,6 +107,7 @@ let setting_values () : setting_value list = [ `B ("xtla", xtla, !xtla); `I ("tb_sl", tb_sl, !tb_sl); `I ("tb_el", tb_el, !tb_el); + `I ("max_threads", max_threads, !max_threads); `B ("cleanfp", cleanfp, !cleanfp); `SO ("fpf_in", fpf_in, !fpf_in); `SO ("fpf_out", fpf_out, !fpf_out); @@ -99,6 +118,7 @@ let setting_values () : setting_value list = [ `B ("suppress_all", suppress_all, !suppress_all); `F ("timeout_stretch", timeout_stretch, !timeout_stretch); `F ("backend_timeout", backend_timeout, !backend_timeout); + `SL ("rev_search_path", rev_search_path, !rev_search_path); ] let default_setting_values = setting_values () @@ -128,13 +148,13 @@ open OUnit2;; let test_help _test_ctxt = reset_setting_values (); let (mods, out, err, exit_code) = parse_args ["--help"] in - assert_equal [] mods; - assert_equal "" out; + assert_equal [] mods ~pp_diff:print_mod_diff; + assert_equal "" out ~pp_diff:print_string_diff; assert_bool "Should print help text" (String.starts_with err ~prefix:"Usage: tlapm FILE"); assert_equal (Some 0) exit_code; let (mods, out, err, exit_code) = parse_args ["-help"] in - assert_equal [] mods; - assert_equal "" out; + assert_equal [] mods ~pp_diff:print_mod_diff; + assert_equal "" out ~pp_diff:print_string_diff; assert_bool "Should print help text" (String.starts_with err ~prefix:"Usage: tlapm FILE"); assert_equal (Some 0) exit_code; assert_equal [] (changed_setting_values ()) ~pp_diff:print_setting_list_diff;; @@ -142,26 +162,26 @@ let test_help _test_ctxt = let test_version _test_ctxt = reset_setting_values (); let (mods, out, err, exit_code) = parse_args ["--version"] in - assert_equal [] mods; + assert_equal [] mods ~pp_diff:print_mod_diff; assert_equal (rawversion () ^ "\n") out; - assert_equal "" err; + assert_equal "" err ~pp_diff:print_string_diff; assert_equal (Some 0) exit_code; assert_equal [] (changed_setting_values ()) ~pp_diff:print_setting_list_diff;; let test_basic _test_ctxt = reset_setting_values (); let (mods, out, err, exit_code) = parse_args ["Test.tla"] in - assert_equal ["Test.tla"] mods; - assert_equal "" out; - assert_equal "" err; + assert_equal ["Test.tla"] mods ~pp_diff:print_mod_diff; + assert_equal "" out ~pp_diff:print_string_diff; + assert_equal "" err ~pp_diff:print_string_diff; assert_equal None exit_code; assert_equal [] (changed_setting_values ()) ~pp_diff:print_setting_list_diff;; let test_no_mods _test_ctxt = reset_setting_values (); let (mods, out, err, exit_code) = parse_args [] in - assert_equal [] mods; - assert_equal "" out; + assert_equal [] mods ~pp_diff:print_mod_diff; + assert_equal "" out ~pp_diff:print_string_diff; assert_bool "Need module req message" (String.starts_with err ~prefix:"Need at least one module file"); assert_equal (Some 2) exit_code; assert_equal [] (changed_setting_values ()) ~pp_diff:print_setting_list_diff;; @@ -169,14 +189,14 @@ let test_no_mods _test_ctxt = let test_verbose _test_ctxt = reset_setting_values (); let (mods, out, err, exit_code) = parse_args ["-v"; "Test.tla"] in - assert_equal ["Test.tla"] mods; + assert_equal ["Test.tla"] mods ~pp_diff:print_mod_diff; assert_bool "Need config" (String.starts_with out ~prefix:"-------------------- tlapm configuration --------------------"); - assert_equal "" err; + assert_equal "" err ~pp_diff:print_string_diff; assert_equal None exit_code; assert_equal [`B ("verbose", verbose, true)] (changed_setting_values ()) ~pp_diff:print_setting_list_diff;; reset_setting_values (); let (mods, out, _err, exit_code) = parse_args ["--verbose"; "Test.tla"] in - assert_equal ["Test.tla"] mods; + assert_equal ["Test.tla"] mods ~pp_diff:print_mod_diff; assert_bool "Need config" (String.starts_with out ~prefix:"-------------------- tlapm configuration --------------------"); (* err probably has output due to being unable to find tools; ignore *) assert_equal None exit_code; @@ -185,16 +205,16 @@ let test_verbose _test_ctxt = let test_where _test_ctxt = reset_setting_values (); let (mods, out, err, exit_code) = parse_args ["--where"] in - assert_equal [] mods; + assert_equal [] mods ~pp_diff:print_mod_diff; assert_bool "Need stlib path" (not (String.equal out "")); - assert_equal "" err; + assert_equal "" err ~pp_diff:print_string_diff; assert_equal (Some 0) exit_code; assert_equal [] (changed_setting_values ()) ~pp_diff:print_setting_list_diff;; let test_config _test_ctxt = reset_setting_values (); let (mods, out, _err, exit_code) = parse_args ["--config"] in - assert_equal [] mods; + assert_equal [] mods ~pp_diff:print_mod_diff; assert_bool "Need config" (String.starts_with out ~prefix:"-------------------- tlapm configuration --------------------"); (* err probably has output due to being unable to find tools; ignore *) assert_equal (Some 0) exit_code; @@ -203,28 +223,87 @@ let test_config _test_ctxt = let test_summary _test_ctxt = reset_setting_values (); let (mods, out, err, exit_code) = parse_args ["--summary"; "Test.tla"] in - assert_equal ["Test.tla"] mods; - assert_equal "" out; - assert_equal "" err; + assert_equal ["Test.tla"] mods ~pp_diff:print_mod_diff; + assert_equal "" out ~pp_diff:print_string_diff; + assert_equal "" err ~pp_diff:print_string_diff; assert_equal None exit_code; assert_equal [`B ("summary", summary, true); `B ("suppress_all", suppress_all, true)] (changed_setting_values ()) ~pp_diff:print_setting_list_diff; assert_equal false !check;; +let test_timing _test_ctxt = + reset_setting_values (); + let (mods, out, err, exit_code) = parse_args ["--timing"; "Test.tla"] in + assert_equal ["Test.tla"] mods ~pp_diff:print_mod_diff; + assert_equal "" out ~pp_diff:print_string_diff; + assert_equal "" err ~pp_diff:print_string_diff; + assert_equal None exit_code; + assert_equal [`B ("stats", stats, true)] (changed_setting_values ()) ~pp_diff:print_setting_list_diff;; + +let test_search_paths _test_ctxt = + reset_setting_values (); + let (mods, out, err, exit_code) = parse_args ["-I"; "some/module/path"; "-I"; "some/other/module/path"; "Test.tla"] in + assert_equal ["Test.tla"] mods ~pp_diff:print_mod_diff; + assert_equal "" out ~pp_diff:print_string_diff; + assert_equal "" err ~pp_diff:print_string_diff; + assert_equal None exit_code; + match changed_setting_values () with + | [`SL ("rev_search_path", _, [_; first_path; second_path])] -> + assert_bool "Should have first path" (string_contains "some/other/module/path" first_path); + assert_bool "Should have second path" (string_contains "some/module/path" second_path) + | _ -> assert_failure "Only search path should have been updated";; + +let test_keep_going _test_ctxt = + reset_setting_values (); + let (mods, out, err, exit_code) = parse_args ["-k"; "Test.tla"] in + assert_equal ["Test.tla"] mods ~pp_diff:print_mod_diff; + assert_equal "" out ~pp_diff:print_string_diff; + assert_equal "" err ~pp_diff:print_string_diff; + assert_equal None exit_code; + assert_equal [`B ("keep_going", keep_going, true)] (changed_setting_values ()) ~pp_diff:print_setting_list_diff;; + +let test_suppress_all _test_ctxt = + reset_setting_values (); + let (mods, out, err, exit_code) = parse_args ["-N"; "Test.tla"] in + assert_equal ["Test.tla"] mods ~pp_diff:print_mod_diff; + assert_equal "" out ~pp_diff:print_string_diff; + assert_equal "" err ~pp_diff:print_string_diff; + assert_equal None exit_code; + assert_equal [`B ("suppress_all", suppress_all, true)] (changed_setting_values ()) ~pp_diff:print_setting_list_diff;; + +let test_use_isabelle_tla _test_ctxt = + reset_setting_values (); + let (mods, out, err, exit_code) = parse_args ["-C"; "Test.tla"] in + assert_equal ["Test.tla"] mods ~pp_diff:print_mod_diff; + assert_equal "" out ~pp_diff:print_string_diff; + assert_equal "" err ~pp_diff:print_string_diff; + assert_equal None exit_code; + assert_equal [`B ("check", check, true)] (changed_setting_values ()) ~pp_diff:print_setting_list_diff;; + +let test_set_max_threads _test_ctxt = + reset_setting_values (); + let thread_count = !max_threads + 1 in + let (mods, out, err, exit_code) = parse_args ["--threads"; Int.to_string thread_count; "Test.tla"] in + assert_equal ["Test.tla"] mods ~pp_diff:print_mod_diff; + assert_equal "" out ~pp_diff:print_string_diff; + assert_equal "" err ~pp_diff:print_string_diff; + assert_equal None exit_code; + assert_equal [`I ("max_threads", max_threads, thread_count)] (changed_setting_values ()) ~pp_diff:print_setting_list_diff;; + let test_use_stdin _test_ctxt = reset_setting_values (); let (mods, out, err, exit_code) = parse_args ["--stdin"; "Test.tla"] in - assert_equal ["Test.tla"] mods; - assert_equal "" out; - assert_equal "" err; + assert_equal ["Test.tla"] mods ~pp_diff:print_mod_diff; + assert_equal "" out ~pp_diff:print_string_diff; + assert_equal "" err ~pp_diff:print_string_diff; assert_equal None exit_code; assert_equal [`B ("use_stdin", use_stdin, true)] (changed_setting_values ()) ~pp_diff:print_setting_list_diff;; let test_prefer_stdlib _test_ctxt = reset_setting_values (); let (mods, out, err, exit_code) = parse_args ["--prefer-stdlib"; "Test.tla"] in - assert_equal ["Test.tla"] mods; - assert_equal "" out; - assert_equal "" err; + assert_equal ["Test.tla"] mods ~pp_diff:print_mod_diff; + assert_equal "" out ~pp_diff:print_string_diff; + assert_equal "" err ~pp_diff:print_string_diff; assert_equal None exit_code; assert_equal [`B ("prefer_stdlib", prefer_stdlib, true)] (changed_setting_values ()) ~pp_diff:print_setting_list_diff;; @@ -237,6 +316,12 @@ let cli_test_suite = "Test CLI Parsing" >::: [ "Print Stlib Location Test" >:: test_where; "Print Config Test" >:: test_config; "Print Summary Test" >:: test_summary; + "Print Stats Test" >:: test_timing; + "Search Paths Test" >:: test_search_paths; + "Keep Going Test" >:: test_keep_going; + "Suppress All Test" >:: test_suppress_all; + "Isabelle/TLA+ Check Test" >:: test_use_isabelle_tla; + "Max Threads Test" >:: test_set_max_threads; "Use Stdin Test" >:: test_use_stdin; "Prefer Stdlib Test" >:: test_prefer_stdlib; ];; From 3f9766c1201d56357caf281d5cd6ad1d1ecac105 Mon Sep 17 00:00:00 2001 From: Andrew Helwer Date: Thu, 27 Nov 2025 19:16:50 -0800 Subject: [PATCH 08/11] Wrote tests for nearly all CLI parameters Signed-off-by: Andrew Helwer --- src/tlapm_args.ml | 16 ++- test/cli/cli_tests.ml | 236 +++++++++++++++++++++++++++++++++++++++++- 2 files changed, 242 insertions(+), 10 deletions(-) diff --git a/src/tlapm_args.ml b/src/tlapm_args.ml index a01f5694e..8969cd153 100644 --- a/src/tlapm_args.ml +++ b/src/tlapm_args.ml @@ -64,7 +64,7 @@ let parse_args executable_name args opts mods usage_fmt err terminate = let show_where out terminate = match stdlib_path with | Some path -> - Printf.sprintf "%s\n" path |> Format.pp_print_text out; + Format.fprintf out "%s\n" path; terminate 0 | None -> Format.pp_print_text out "N/A\n"; @@ -268,16 +268,14 @@ let init ?(out=Format.std_formatter) ?(err=Format.err_formatter) ?(terminate=exi end ; check_zenon_ver () ; if !Params.toolbox then begin - Printf.sprintf "\n\\* TLAPM version %s\n" - (Params.rawversion ()) - |> Format.pp_print_text out; + Format.fprintf out "\n\\* TLAPM version %s\n" + (Params.rawversion ()); let tm = Unix.localtime (Unix.gettimeofday ()) in - Printf.sprintf "\\* launched at %04d-%02d-%02d %02d:%02d:%02d" + Format.fprintf out "\\* launched at %04d-%02d-%02d %02d:%02d:%02d" (tm.Unix.tm_year + 1900) (tm.Unix.tm_mon + 1) tm.Unix.tm_mday - tm.Unix.tm_hour tm.Unix.tm_min tm.Unix.tm_sec - |> Format.pp_print_text out; - Printf.sprintf " with command line:\n\\*" |> Format.pp_print_text out; - Array.iter (fun s -> Printf.sprintf " %s" (quote_if_needed s) |> Format.pp_print_text out) args; + tm.Unix.tm_hour tm.Unix.tm_min tm.Unix.tm_sec; + Format.fprintf out " with command line:\n\\*"; + Array.iter (fun s -> Format.fprintf out " %s" (quote_if_needed s)) args; Format.pp_print_text out "\n\n%!" end; if !use_stdin && (List.length !mods) <> 1 then begin diff --git a/test/cli/cli_tests.ml b/test/cli/cli_tests.ml index eee431d36..a644800c8 100644 --- a/test/cli/cli_tests.ml +++ b/test/cli/cli_tests.ml @@ -8,8 +8,17 @@ type setting_value = [ | `S of string * string ref * string | `SO of string * string option ref * string option | `SL of string * string list ref * string list + | `ML of string * Tlapm_lib__Method.t list ref * Tlapm_lib__Method.t list ] +let capture_output (f : Format.formatter -> unit) : string = + let out = Buffer.create 0 in + let out_format = Format.formatter_of_buffer out in + f out_format; + Format.pp_print_flush out_format (); + Buffer.contents out + + let rec string_contains (needle : string) (haystack : string) : bool = match haystack with | "" -> false @@ -18,7 +27,7 @@ let rec string_contains (needle : string) (haystack : string) : bool = string_contains needle let str_ls_as_str (ls : string list) : string = - List.fold_left (^) "[" ls + "[" ^ (String.concat "; " ls) ^ "]" let display_setting_value (v : setting_value) : string = match v with @@ -28,6 +37,7 @@ let display_setting_value (v : setting_value) : string = | `S (n, rf, v) -> Printf.sprintf "%s: %s [%s]" n v !rf | `SO (n, rf, v) -> Printf.sprintf "%s: %s [%s]" n (Option.value ~default:"None" v) (Option.value ~default:"None" !rf) | `SL (n, rf, v) -> Printf.sprintf "%s: %s [%s]" n (str_ls_as_str v) (str_ls_as_str !rf) + | `ML (n, rf, v) -> Printf.sprintf "%s: %s [%s]" n (str_ls_as_str (List.map (fun m -> capture_output (fun f -> Tlapm_lib__Method.pp_print_tactic f m)) v)) (str_ls_as_str (List.map (fun m -> capture_output (fun f -> Tlapm_lib__Method.pp_print_tactic f m)) !rf)) let print_string_diff (formatter : Format.formatter) ((expected, actual) : string * string) : unit = Printf.sprintf "exp/act: (%s)/(%s)" expected actual |> Format.pp_print_text formatter @@ -59,6 +69,7 @@ let setting_value_changed (setting : setting_value) = | `S (_, rf, v) -> not (!rf = v) | `SO (_, rf, v) -> not (!rf = v) | `SL (_, rf, v) -> not (List.equal String.equal !rf v) + | `ML (_, rf, v) -> not (!rf = v) let changed_setting_value (setting : setting_value) = if setting_value_changed setting then @@ -69,6 +80,7 @@ let changed_setting_value (setting : setting_value) = | `S (n, rf, _) -> Some (`S (n, rf, !rf)) | `SO (n, rf, _) -> Some (`SO (n, rf, !rf)) | `SL (n, rf, _) -> Some (`SL (n, rf, !rf)) + | `ML (n, rf, _) -> Some (`ML (n, rf, !rf)) else None let set_setting_value (setting : setting_value) = @@ -79,6 +91,7 @@ let set_setting_value (setting : setting_value) = | `S (_, rf, v) -> rf := v | `SO (_, rf, v) -> rf := v | `SL (_, rf, v) -> rf := v + | `ML (_, rf, v) -> rf := v open Tlapm_lib__Params;; @@ -119,6 +132,9 @@ let setting_values () : setting_value list = [ `F ("timeout_stretch", timeout_stretch, !timeout_stretch); `F ("backend_timeout", backend_timeout, !backend_timeout); `SL ("rev_search_path", rev_search_path, !rev_search_path); + `ML ("default_method", default_method, !default_method); + `S ("smt_logic", smt_logic, !smt_logic); + `S ("cachedir", cachedir, !cachedir); ] let default_setting_values = setting_values () @@ -289,6 +305,117 @@ let test_set_max_threads _test_ctxt = assert_equal None exit_code; assert_equal [`I ("max_threads", max_threads, thread_count)] (changed_setting_values ()) ~pp_diff:print_setting_list_diff;; +let test_set_method _text_ctxt = + reset_setting_values (); + let (mods, out, err, exit_code) = parse_args ["--method"; "fail"; "Test.tla"] in + assert_equal ["Test.tla"] mods ~pp_diff:print_mod_diff; + assert_equal "" out ~pp_diff:print_string_diff; + assert_equal "" err ~pp_diff:print_string_diff; + assert_equal None exit_code; + assert_equal [`ML ("default_method", default_method, [Tlapm_lib__Method.Fail])] (changed_setting_values ()) ~pp_diff:print_setting_list_diff;; + +let test_set_solver _test_ctxt = + reset_setting_values (); + let solver_cmd = "my_solver_cmd" in + let (mods, out, err, exit_code) = parse_args ["--solver"; solver_cmd; "Test.tla"] in + assert_equal ["Test.tla"] mods ~pp_diff:print_mod_diff; + assert_equal "" out ~pp_diff:print_string_diff; + assert_equal "" err ~pp_diff:print_string_diff; + assert_equal None exit_code; + assert_equal [] (changed_setting_values ()) ~pp_diff:print_setting_list_diff; + (* Params.exec is unfortunately an opaque type whose value we cannot directly access *) + assert_bool "Solver command should be custom" (string_contains solver_cmd (solve_cmd smt "file.tla"));; + +let test_set_smt_logic _test_ctxt = + reset_setting_values (); + let expected_smt_logic = "my_smt_logic" in + let (mods, out, err, exit_code) = parse_args ["--smt-logic"; expected_smt_logic; "Test.tla"] in + assert_equal ["Test.tla"] mods ~pp_diff:print_mod_diff; + assert_equal "" out ~pp_diff:print_string_diff; + assert_equal "" err ~pp_diff:print_string_diff; + assert_equal None exit_code; + assert_equal [`S ("smt_logic", smt_logic, expected_smt_logic)] (changed_setting_values ()) ~pp_diff:print_setting_list_diff;; + +let test_stretch _test_ctxt = + reset_setting_values (); + let expected_stretch = Float.add !timeout_stretch 1.0 in + let (mods, out, err, exit_code) = parse_args ["--stretch"; Float.to_string expected_stretch; "Test.tla"] in + assert_equal ["Test.tla"] mods ~pp_diff:print_mod_diff; + assert_equal "" out ~pp_diff:print_string_diff; + assert_equal "" err ~pp_diff:print_string_diff; + assert_equal None exit_code; + assert_equal [`F ("timeout_stretch", timeout_stretch, expected_stretch)] (changed_setting_values ()) ~pp_diff:print_setting_list_diff;; + +let test_no_flatten _test_ctxt = + reset_setting_values (); + let (mods, out, err, exit_code) = parse_args ["--noflatten"; "Test.tla"] in + assert_equal ["Test.tla"] mods ~pp_diff:print_mod_diff; + assert_equal "" out ~pp_diff:print_string_diff; + assert_equal "" err ~pp_diff:print_string_diff; + assert_equal None exit_code; + assert_equal [`B ("ob_flatten", ob_flatten, false)] (changed_setting_values ()) ~pp_diff:print_setting_list_diff;; + +let test_no_normalize _test_ctxt = + reset_setting_values (); + let (mods, out, err, exit_code) = parse_args ["--nonormal"; "Test.tla"] in + assert_equal ["Test.tla"] mods ~pp_diff:print_mod_diff; + assert_equal "" out ~pp_diff:print_string_diff; + assert_equal "" err ~pp_diff:print_string_diff; + assert_equal None exit_code; + assert_equal [`B ("pr_normal", pr_normal, false)] (changed_setting_values ()) ~pp_diff:print_setting_list_diff;; + +let test_debug_flags _test_ctxt = + reset_setting_values (); + let expected_debug_flags = ["foo"; "bar"; "baz"] in + let (mods, out, err, exit_code) = parse_args ["--debug"; String.concat "," expected_debug_flags; "Test.tla"] in + assert_equal ["Test.tla"] mods ~pp_diff:print_mod_diff; + assert_equal "" out ~pp_diff:print_string_diff; + assert_equal "" err ~pp_diff:print_string_diff; + assert_equal None exit_code; + assert_equal [] (changed_setting_values ()) ~pp_diff:print_setting_list_diff; + List.iter (fun flag -> assert_bool flag (debugging flag)) expected_debug_flags; + List.iter rm_debug_flag expected_debug_flags;; + +let test_toolbox_mode _test_ctxt = + reset_setting_values (); + let (tb_start, tb_end) = (1, 2) in + let (mods, out, err, exit_code) = parse_args ["--toolbox"; Int.to_string tb_start; Int.to_string tb_end; "Test.tla"] in + assert_equal ["Test.tla"] mods ~pp_diff:print_mod_diff; + assert_bool "Expect toolbox output" (out <> ""); + assert_equal "" err ~pp_diff:print_string_diff; + assert_equal None exit_code; + assert_equal [`B ("toolbox", toolbox, true); `I ("tb_sl", tb_sl, tb_start); `I ("tb_el", tb_el, tb_end)] (changed_setting_values ()) ~pp_diff:print_setting_list_diff;; + +let test_toolbox_protocol_version _test_ctxt = + reset_setting_values (); + let expected_toolbox_version = 3 in + let (mods, out, err, exit_code) = parse_args ["--toolbox-vsn"; Int.to_string expected_toolbox_version; "Test.tla"] in + assert_equal ["Test.tla"] mods ~pp_diff:print_mod_diff; + assert_bool "Expect toolbox output" (out <> ""); + assert_equal "" err ~pp_diff:print_string_diff; + assert_equal None exit_code; + assert_equal [`B ("toolbox", toolbox, true); `I ("toolbox_vsn", toolbox_vsn, expected_toolbox_version)] (changed_setting_values ()) ~pp_diff:print_setting_list_diff;; + +let test_line _test_ctxt = + reset_setting_values (); + let expected_line = 10 in + let (mods, out, err, exit_code) = parse_args ["--line"; Int.to_string expected_line; "Test.tla"] in + assert_equal ["Test.tla"] mods ~pp_diff:print_mod_diff; + assert_bool "Expect toolbox output" (out <> ""); + assert_equal "" err ~pp_diff:print_string_diff; + assert_equal None exit_code; + assert_equal [`B ("toolbox", toolbox, true); `I ("tb_sl", tb_sl, expected_line); `I ("tb_el", tb_el, expected_line)] (changed_setting_values ()) ~pp_diff:print_setting_list_diff;; + +let test_wait _test_ctxt = + reset_setting_values (); + let expected_wait = 30 in + let (mods, out, err, exit_code) = parse_args ["--wait"; Int.to_string expected_wait; "Test.tla"] in + assert_equal ["Test.tla"] mods ~pp_diff:print_mod_diff; + assert_equal "" out ~pp_diff:print_string_diff; + assert_equal "" err ~pp_diff:print_string_diff; + assert_equal None exit_code; + assert_equal [`I ("wait", wait, expected_wait)] (changed_setting_values ()) ~pp_diff:print_setting_list_diff;; + let test_use_stdin _test_ctxt = reset_setting_values (); let (mods, out, err, exit_code) = parse_args ["--stdin"; "Test.tla"] in @@ -307,6 +434,93 @@ let test_prefer_stdlib _test_ctxt = assert_equal None exit_code; assert_equal [`B ("prefer_stdlib", prefer_stdlib, true)] (changed_setting_values ()) ~pp_diff:print_setting_list_diff;; +let test_no_prove _test_ctxt = + reset_setting_values (); + let (mods, out, err, exit_code) = parse_args ["--noproving"; "Test.tla"] in + assert_equal ["Test.tla"] mods ~pp_diff:print_mod_diff; + assert_equal "" out ~pp_diff:print_string_diff; + assert_equal "" err ~pp_diff:print_string_diff; + assert_equal None exit_code; + assert_equal [`B ("noproving", noproving, true)] (changed_setting_values ()) ~pp_diff:print_setting_list_diff;; + +let test_print_all_obligations _test_ctxt = + reset_setting_values (); + let (mods, out, err, exit_code) = parse_args ["--printallobs"; "Test.tla"] in + assert_equal ["Test.tla"] mods ~pp_diff:print_mod_diff; + assert_equal "" out ~pp_diff:print_string_diff; + assert_equal "" err ~pp_diff:print_string_diff; + assert_equal None exit_code; + assert_equal [`B ("printallobs", printallobs, true)] (changed_setting_values ()) ~pp_diff:print_setting_list_diff;; + +let test_safe_fingerprints _test_ctxt = + reset_setting_values (); + let (mods, out, err, exit_code) = parse_args ["--safefp"; "Test.tla"] in + assert_equal ["Test.tla"] mods ~pp_diff:print_mod_diff; + assert_equal "" out ~pp_diff:print_string_diff; + assert_equal "" err ~pp_diff:print_string_diff; + assert_equal None exit_code; + assert_equal [`B ("safefp", safefp, true)] (changed_setting_values ()) ~pp_diff:print_setting_list_diff;; + +let test_no_fingerprints _test_ctxt = + reset_setting_values (); + let (mods, out, err, exit_code) = parse_args ["--nofp"; "Test.tla"] in + assert_equal ["Test.tla"] mods ~pp_diff:print_mod_diff; + assert_equal "" out ~pp_diff:print_string_diff; + assert_equal "" err ~pp_diff:print_string_diff; + assert_equal None exit_code; + assert_equal [`B ("no_fp", no_fp, true)] (changed_setting_values ()) ~pp_diff:print_setting_list_diff;; + +let test_no_fingerprints_between_lines _test_ctxt = + reset_setting_values (); + let (expected_start, expected_end) = (10, 20) in + let (mods, out, err, exit_code) = parse_args ["--nofpl"; Int.to_string expected_start; Int.to_string expected_end; "Test.tla"] in + assert_equal ["Test.tla"] mods ~pp_diff:print_mod_diff; + assert_equal "" out ~pp_diff:print_string_diff; + assert_equal "" err ~pp_diff:print_string_diff; + assert_equal None exit_code; + assert_equal [`I ("nofp_sl", nofp_sl, expected_start); `I ("nofp_el", nofp_el, expected_end)] (changed_setting_values ()) ~pp_diff:print_setting_list_diff;; + +let test_clean_fingerprints _test_ctxt = + reset_setting_values (); + let (mods, out, err, exit_code) = parse_args ["--cleanfp"; "Test.tla"] in + assert_equal ["Test.tla"] mods ~pp_diff:print_mod_diff; + assert_equal "" out ~pp_diff:print_string_diff; + assert_equal "" err ~pp_diff:print_string_diff; + assert_equal None exit_code; + assert_equal [`B ("cleanfp", cleanfp, true)] (changed_setting_values ()) ~pp_diff:print_setting_list_diff;; + +(* Cannot test --erasefp due to side-effects *) +(* Cannot test --printfp due to side-effects *) + +let test_use_fingerprints _test_ctxt = + reset_setting_values (); + let expected_fp_file = "FingerprintFile.txt" in + let (mods, out, err, exit_code) = parse_args ["--usefp"; expected_fp_file; "Test.tla"] in + assert_equal ["Test.tla"] mods ~pp_diff:print_mod_diff; + assert_equal "" out ~pp_diff:print_string_diff; + assert_equal "" err ~pp_diff:print_string_diff; + assert_equal None exit_code; + assert_equal [`SO ("fpf_in", fpf_in, Some expected_fp_file)] (changed_setting_values ()) ~pp_diff:print_setting_list_diff;; + +let test_fp_deb _test_ctxt = + reset_setting_values (); + let (mods, out, err, exit_code) = parse_args ["--fpp"; "Test.tla"] in + assert_equal ["Test.tla"] mods ~pp_diff:print_mod_diff; + assert_equal "" out ~pp_diff:print_string_diff; + assert_equal "" err ~pp_diff:print_string_diff; + assert_equal None exit_code; + assert_equal [`B ("fp_deb", fp_deb, true)] (changed_setting_values ()) ~pp_diff:print_setting_list_diff;; + +let test_cache_dir _test_ctxt = + reset_setting_values (); + let expected_cache_dir = "some/cache/dir" in + let (mods, out, err, exit_code) = parse_args ["--cache-dir"; expected_cache_dir; "Test.tla"] in + assert_equal ["Test.tla"] mods ~pp_diff:print_mod_diff; + assert_equal "" out ~pp_diff:print_string_diff; + assert_equal "" err ~pp_diff:print_string_diff; + assert_equal None exit_code; + assert_equal [`S ("cachedir", cachedir, expected_cache_dir)] (changed_setting_values ()) ~pp_diff:print_setting_list_diff;; + let cli_test_suite = "Test CLI Parsing" >::: [ "Help Test" >:: test_help; "Basic Test" >:: test_basic; @@ -322,8 +536,28 @@ let cli_test_suite = "Test CLI Parsing" >::: [ "Suppress All Test" >:: test_suppress_all; "Isabelle/TLA+ Check Test" >:: test_use_isabelle_tla; "Max Threads Test" >:: test_set_max_threads; + "Set Method Test" >:: test_set_method; + "Custom Solver Test" >:: test_set_solver; + "Custom SMT Logic Test" >:: test_set_smt_logic; + "Stretch Test" >:: test_stretch; + "No Flatten Test" >:: test_no_flatten; + "No Normalize Test" >:: test_no_normalize; + "Debug Flag Test" >:: test_debug_flags; + "Toolbox Mode Test" >:: test_toolbox_mode; + "Toolbox Protocol Version Test" >:: test_toolbox_protocol_version; + "Check Specific Line Test" >:: test_line; + "Wait Before Printing Obligations Test" >:: test_wait; "Use Stdin Test" >:: test_use_stdin; "Prefer Stdlib Test" >:: test_prefer_stdlib; + "Skip Proving Test" >:: test_no_prove; + "Print All Obligations Test" >:: test_print_all_obligations; + "Safe Fingerprint Check Test" >:: test_safe_fingerprints; + "No Fingerprints Test" >:: test_no_fingerprints; + "No Fingerprints Between Specific Lines Test" >:: test_no_fingerprints_between_lines; + "Clean Fingerprints Test" >:: test_clean_fingerprints; + "Use Specififc Fingerprint File Test" >:: test_use_fingerprints; + "Test Print Fingerprints in Toolbox Messages" >:: test_fp_deb; + "Cache Dir Test" >:: test_cache_dir; ];; let () = run_test_tt_main cli_test_suite From bea4abd5cec8ac8256f5632bfb1a73d9fc12b958 Mon Sep 17 00:00:00 2001 From: Andrew Helwer Date: Fri, 28 Nov 2025 13:30:16 -0800 Subject: [PATCH 09/11] Clean up after CLI tests Signed-off-by: Andrew Helwer --- test/cli/cli_tests.ml | 116 ++++++++++++++++++++++++++++-------------- 1 file changed, 77 insertions(+), 39 deletions(-) diff --git a/test/cli/cli_tests.ml b/test/cli/cli_tests.ml index a644800c8..6c70ab131 100644 --- a/test/cli/cli_tests.ml +++ b/test/cli/cli_tests.ml @@ -173,7 +173,8 @@ let test_help _test_ctxt = assert_equal "" out ~pp_diff:print_string_diff; assert_bool "Should print help text" (String.starts_with err ~prefix:"Usage: tlapm FILE"); assert_equal (Some 0) exit_code; - assert_equal [] (changed_setting_values ()) ~pp_diff:print_setting_list_diff;; + assert_equal [] (changed_setting_values ()) ~pp_diff:print_setting_list_diff; + reset_setting_values ();; let test_version _test_ctxt = reset_setting_values (); @@ -182,7 +183,8 @@ let test_version _test_ctxt = assert_equal (rawversion () ^ "\n") out; assert_equal "" err ~pp_diff:print_string_diff; assert_equal (Some 0) exit_code; - assert_equal [] (changed_setting_values ()) ~pp_diff:print_setting_list_diff;; + assert_equal [] (changed_setting_values ()) ~pp_diff:print_setting_list_diff; + reset_setting_values ();; let test_basic _test_ctxt = reset_setting_values (); @@ -191,7 +193,8 @@ let test_basic _test_ctxt = assert_equal "" out ~pp_diff:print_string_diff; assert_equal "" err ~pp_diff:print_string_diff; assert_equal None exit_code; - assert_equal [] (changed_setting_values ()) ~pp_diff:print_setting_list_diff;; + assert_equal [] (changed_setting_values ()) ~pp_diff:print_setting_list_diff; + reset_setting_values ();; let test_no_mods _test_ctxt = reset_setting_values (); @@ -200,7 +203,8 @@ let test_no_mods _test_ctxt = assert_equal "" out ~pp_diff:print_string_diff; assert_bool "Need module req message" (String.starts_with err ~prefix:"Need at least one module file"); assert_equal (Some 2) exit_code; - assert_equal [] (changed_setting_values ()) ~pp_diff:print_setting_list_diff;; + assert_equal [] (changed_setting_values ()) ~pp_diff:print_setting_list_diff; + reset_setting_values ();; let test_verbose _test_ctxt = reset_setting_values (); @@ -216,7 +220,8 @@ let test_verbose _test_ctxt = assert_bool "Need config" (String.starts_with out ~prefix:"-------------------- tlapm configuration --------------------"); (* err probably has output due to being unable to find tools; ignore *) assert_equal None exit_code; - assert_equal [`B ("verbose", verbose, true)] (changed_setting_values ()) ~pp_diff:print_setting_list_diff;; + assert_equal [`B ("verbose", verbose, true)] (changed_setting_values ()) ~pp_diff:print_setting_list_diff; + reset_setting_values ();; let test_where _test_ctxt = reset_setting_values (); @@ -225,7 +230,8 @@ let test_where _test_ctxt = assert_bool "Need stlib path" (not (String.equal out "")); assert_equal "" err ~pp_diff:print_string_diff; assert_equal (Some 0) exit_code; - assert_equal [] (changed_setting_values ()) ~pp_diff:print_setting_list_diff;; + assert_equal [] (changed_setting_values ()) ~pp_diff:print_setting_list_diff; + reset_setting_values ();; let test_config _test_ctxt = reset_setting_values (); @@ -234,7 +240,8 @@ let test_config _test_ctxt = assert_bool "Need config" (String.starts_with out ~prefix:"-------------------- tlapm configuration --------------------"); (* err probably has output due to being unable to find tools; ignore *) assert_equal (Some 0) exit_code; - assert_equal [] (changed_setting_values ()) ~pp_diff:print_setting_list_diff;; + assert_equal [] (changed_setting_values ()) ~pp_diff:print_setting_list_diff; + reset_setting_values ();; let test_summary _test_ctxt = reset_setting_values (); @@ -244,7 +251,8 @@ let test_summary _test_ctxt = assert_equal "" err ~pp_diff:print_string_diff; assert_equal None exit_code; assert_equal [`B ("summary", summary, true); `B ("suppress_all", suppress_all, true)] (changed_setting_values ()) ~pp_diff:print_setting_list_diff; - assert_equal false !check;; + assert_equal false !check; + reset_setting_values ();; let test_timing _test_ctxt = reset_setting_values (); @@ -253,9 +261,10 @@ let test_timing _test_ctxt = assert_equal "" out ~pp_diff:print_string_diff; assert_equal "" err ~pp_diff:print_string_diff; assert_equal None exit_code; - assert_equal [`B ("stats", stats, true)] (changed_setting_values ()) ~pp_diff:print_setting_list_diff;; + assert_equal [`B ("stats", stats, true)] (changed_setting_values ()) ~pp_diff:print_setting_list_diff; + reset_setting_values ();; -let test_search_paths _test_ctxt = +let test_search_paths _test_ctxt : unit = reset_setting_values (); let (mods, out, err, exit_code) = parse_args ["-I"; "some/module/path"; "-I"; "some/other/module/path"; "Test.tla"] in assert_equal ["Test.tla"] mods ~pp_diff:print_mod_diff; @@ -265,8 +274,9 @@ let test_search_paths _test_ctxt = match changed_setting_values () with | [`SL ("rev_search_path", _, [_; first_path; second_path])] -> assert_bool "Should have first path" (string_contains "some/other/module/path" first_path); - assert_bool "Should have second path" (string_contains "some/module/path" second_path) - | _ -> assert_failure "Only search path should have been updated";; + assert_bool "Should have second path" (string_contains "some/module/path" second_path); + | _ -> assert_bool "Search path not as expected" false; + reset_setting_values ();; let test_keep_going _test_ctxt = reset_setting_values (); @@ -275,7 +285,8 @@ let test_keep_going _test_ctxt = assert_equal "" out ~pp_diff:print_string_diff; assert_equal "" err ~pp_diff:print_string_diff; assert_equal None exit_code; - assert_equal [`B ("keep_going", keep_going, true)] (changed_setting_values ()) ~pp_diff:print_setting_list_diff;; + assert_equal [`B ("keep_going", keep_going, true)] (changed_setting_values ()) ~pp_diff:print_setting_list_diff; + reset_setting_values ();; let test_suppress_all _test_ctxt = reset_setting_values (); @@ -284,7 +295,8 @@ let test_suppress_all _test_ctxt = assert_equal "" out ~pp_diff:print_string_diff; assert_equal "" err ~pp_diff:print_string_diff; assert_equal None exit_code; - assert_equal [`B ("suppress_all", suppress_all, true)] (changed_setting_values ()) ~pp_diff:print_setting_list_diff;; + assert_equal [`B ("suppress_all", suppress_all, true)] (changed_setting_values ()) ~pp_diff:print_setting_list_diff; + reset_setting_values ();; let test_use_isabelle_tla _test_ctxt = reset_setting_values (); @@ -293,7 +305,8 @@ let test_use_isabelle_tla _test_ctxt = assert_equal "" out ~pp_diff:print_string_diff; assert_equal "" err ~pp_diff:print_string_diff; assert_equal None exit_code; - assert_equal [`B ("check", check, true)] (changed_setting_values ()) ~pp_diff:print_setting_list_diff;; + assert_equal [`B ("check", check, true)] (changed_setting_values ()) ~pp_diff:print_setting_list_diff; + reset_setting_values ();; let test_set_max_threads _test_ctxt = reset_setting_values (); @@ -303,7 +316,8 @@ let test_set_max_threads _test_ctxt = assert_equal "" out ~pp_diff:print_string_diff; assert_equal "" err ~pp_diff:print_string_diff; assert_equal None exit_code; - assert_equal [`I ("max_threads", max_threads, thread_count)] (changed_setting_values ()) ~pp_diff:print_setting_list_diff;; + assert_equal [`I ("max_threads", max_threads, thread_count)] (changed_setting_values ()) ~pp_diff:print_setting_list_diff; + reset_setting_values ();; let test_set_method _text_ctxt = reset_setting_values (); @@ -312,8 +326,10 @@ let test_set_method _text_ctxt = assert_equal "" out ~pp_diff:print_string_diff; assert_equal "" err ~pp_diff:print_string_diff; assert_equal None exit_code; - assert_equal [`ML ("default_method", default_method, [Tlapm_lib__Method.Fail])] (changed_setting_values ()) ~pp_diff:print_setting_list_diff;; + assert_equal [`ML ("default_method", default_method, [Tlapm_lib__Method.Fail])] (changed_setting_values ()) ~pp_diff:print_setting_list_diff; + reset_setting_values ();; +(* let test_set_solver _test_ctxt = reset_setting_values (); let solver_cmd = "my_solver_cmd" in @@ -324,7 +340,9 @@ let test_set_solver _test_ctxt = assert_equal None exit_code; assert_equal [] (changed_setting_values ()) ~pp_diff:print_setting_list_diff; (* Params.exec is unfortunately an opaque type whose value we cannot directly access *) - assert_bool "Solver command should be custom" (string_contains solver_cmd (solve_cmd smt "file.tla"));; + assert_bool "Solver command should be custom" (string_contains solver_cmd (solve_cmd smt "file.tla")); + reset_setting_values ();; +*) let test_set_smt_logic _test_ctxt = reset_setting_values (); @@ -334,7 +352,8 @@ let test_set_smt_logic _test_ctxt = assert_equal "" out ~pp_diff:print_string_diff; assert_equal "" err ~pp_diff:print_string_diff; assert_equal None exit_code; - assert_equal [`S ("smt_logic", smt_logic, expected_smt_logic)] (changed_setting_values ()) ~pp_diff:print_setting_list_diff;; + assert_equal [`S ("smt_logic", smt_logic, expected_smt_logic)] (changed_setting_values ()) ~pp_diff:print_setting_list_diff; + reset_setting_values ();; let test_stretch _test_ctxt = reset_setting_values (); @@ -344,7 +363,8 @@ let test_stretch _test_ctxt = assert_equal "" out ~pp_diff:print_string_diff; assert_equal "" err ~pp_diff:print_string_diff; assert_equal None exit_code; - assert_equal [`F ("timeout_stretch", timeout_stretch, expected_stretch)] (changed_setting_values ()) ~pp_diff:print_setting_list_diff;; + assert_equal [`F ("timeout_stretch", timeout_stretch, expected_stretch)] (changed_setting_values ()) ~pp_diff:print_setting_list_diff; + reset_setting_values ();; let test_no_flatten _test_ctxt = reset_setting_values (); @@ -353,7 +373,8 @@ let test_no_flatten _test_ctxt = assert_equal "" out ~pp_diff:print_string_diff; assert_equal "" err ~pp_diff:print_string_diff; assert_equal None exit_code; - assert_equal [`B ("ob_flatten", ob_flatten, false)] (changed_setting_values ()) ~pp_diff:print_setting_list_diff;; + assert_equal [`B ("ob_flatten", ob_flatten, false)] (changed_setting_values ()) ~pp_diff:print_setting_list_diff; + reset_setting_values ();; let test_no_normalize _test_ctxt = reset_setting_values (); @@ -362,7 +383,8 @@ let test_no_normalize _test_ctxt = assert_equal "" out ~pp_diff:print_string_diff; assert_equal "" err ~pp_diff:print_string_diff; assert_equal None exit_code; - assert_equal [`B ("pr_normal", pr_normal, false)] (changed_setting_values ()) ~pp_diff:print_setting_list_diff;; + assert_equal [`B ("pr_normal", pr_normal, false)] (changed_setting_values ()) ~pp_diff:print_setting_list_diff; + reset_setting_values ();; let test_debug_flags _test_ctxt = reset_setting_values (); @@ -374,7 +396,8 @@ let test_debug_flags _test_ctxt = assert_equal None exit_code; assert_equal [] (changed_setting_values ()) ~pp_diff:print_setting_list_diff; List.iter (fun flag -> assert_bool flag (debugging flag)) expected_debug_flags; - List.iter rm_debug_flag expected_debug_flags;; + List.iter rm_debug_flag expected_debug_flags; + reset_setting_values ();; let test_toolbox_mode _test_ctxt = reset_setting_values (); @@ -384,7 +407,8 @@ let test_toolbox_mode _test_ctxt = assert_bool "Expect toolbox output" (out <> ""); assert_equal "" err ~pp_diff:print_string_diff; assert_equal None exit_code; - assert_equal [`B ("toolbox", toolbox, true); `I ("tb_sl", tb_sl, tb_start); `I ("tb_el", tb_el, tb_end)] (changed_setting_values ()) ~pp_diff:print_setting_list_diff;; + assert_equal [`B ("toolbox", toolbox, true); `I ("tb_sl", tb_sl, tb_start); `I ("tb_el", tb_el, tb_end)] (changed_setting_values ()) ~pp_diff:print_setting_list_diff; + reset_setting_values ();; let test_toolbox_protocol_version _test_ctxt = reset_setting_values (); @@ -394,7 +418,8 @@ let test_toolbox_protocol_version _test_ctxt = assert_bool "Expect toolbox output" (out <> ""); assert_equal "" err ~pp_diff:print_string_diff; assert_equal None exit_code; - assert_equal [`B ("toolbox", toolbox, true); `I ("toolbox_vsn", toolbox_vsn, expected_toolbox_version)] (changed_setting_values ()) ~pp_diff:print_setting_list_diff;; + assert_equal [`B ("toolbox", toolbox, true); `I ("toolbox_vsn", toolbox_vsn, expected_toolbox_version)] (changed_setting_values ()) ~pp_diff:print_setting_list_diff; + reset_setting_values ();; let test_line _test_ctxt = reset_setting_values (); @@ -404,7 +429,8 @@ let test_line _test_ctxt = assert_bool "Expect toolbox output" (out <> ""); assert_equal "" err ~pp_diff:print_string_diff; assert_equal None exit_code; - assert_equal [`B ("toolbox", toolbox, true); `I ("tb_sl", tb_sl, expected_line); `I ("tb_el", tb_el, expected_line)] (changed_setting_values ()) ~pp_diff:print_setting_list_diff;; + assert_equal [`B ("toolbox", toolbox, true); `I ("tb_sl", tb_sl, expected_line); `I ("tb_el", tb_el, expected_line)] (changed_setting_values ()) ~pp_diff:print_setting_list_diff; + reset_setting_values ();; let test_wait _test_ctxt = reset_setting_values (); @@ -414,7 +440,8 @@ let test_wait _test_ctxt = assert_equal "" out ~pp_diff:print_string_diff; assert_equal "" err ~pp_diff:print_string_diff; assert_equal None exit_code; - assert_equal [`I ("wait", wait, expected_wait)] (changed_setting_values ()) ~pp_diff:print_setting_list_diff;; + assert_equal [`I ("wait", wait, expected_wait)] (changed_setting_values ()) ~pp_diff:print_setting_list_diff; + reset_setting_values ();; let test_use_stdin _test_ctxt = reset_setting_values (); @@ -423,7 +450,8 @@ let test_use_stdin _test_ctxt = assert_equal "" out ~pp_diff:print_string_diff; assert_equal "" err ~pp_diff:print_string_diff; assert_equal None exit_code; - assert_equal [`B ("use_stdin", use_stdin, true)] (changed_setting_values ()) ~pp_diff:print_setting_list_diff;; + assert_equal [`B ("use_stdin", use_stdin, true)] (changed_setting_values ()) ~pp_diff:print_setting_list_diff; + reset_setting_values ();; let test_prefer_stdlib _test_ctxt = reset_setting_values (); @@ -432,7 +460,8 @@ let test_prefer_stdlib _test_ctxt = assert_equal "" out ~pp_diff:print_string_diff; assert_equal "" err ~pp_diff:print_string_diff; assert_equal None exit_code; - assert_equal [`B ("prefer_stdlib", prefer_stdlib, true)] (changed_setting_values ()) ~pp_diff:print_setting_list_diff;; + assert_equal [`B ("prefer_stdlib", prefer_stdlib, true)] (changed_setting_values ()) ~pp_diff:print_setting_list_diff; + reset_setting_values ();; let test_no_prove _test_ctxt = reset_setting_values (); @@ -441,7 +470,8 @@ let test_no_prove _test_ctxt = assert_equal "" out ~pp_diff:print_string_diff; assert_equal "" err ~pp_diff:print_string_diff; assert_equal None exit_code; - assert_equal [`B ("noproving", noproving, true)] (changed_setting_values ()) ~pp_diff:print_setting_list_diff;; + assert_equal [`B ("noproving", noproving, true)] (changed_setting_values ()) ~pp_diff:print_setting_list_diff; + reset_setting_values ();; let test_print_all_obligations _test_ctxt = reset_setting_values (); @@ -450,7 +480,8 @@ let test_print_all_obligations _test_ctxt = assert_equal "" out ~pp_diff:print_string_diff; assert_equal "" err ~pp_diff:print_string_diff; assert_equal None exit_code; - assert_equal [`B ("printallobs", printallobs, true)] (changed_setting_values ()) ~pp_diff:print_setting_list_diff;; + assert_equal [`B ("printallobs", printallobs, true)] (changed_setting_values ()) ~pp_diff:print_setting_list_diff; + reset_setting_values ();; let test_safe_fingerprints _test_ctxt = reset_setting_values (); @@ -459,7 +490,8 @@ let test_safe_fingerprints _test_ctxt = assert_equal "" out ~pp_diff:print_string_diff; assert_equal "" err ~pp_diff:print_string_diff; assert_equal None exit_code; - assert_equal [`B ("safefp", safefp, true)] (changed_setting_values ()) ~pp_diff:print_setting_list_diff;; + assert_equal [`B ("safefp", safefp, true)] (changed_setting_values ()) ~pp_diff:print_setting_list_diff; + reset_setting_values ();; let test_no_fingerprints _test_ctxt = reset_setting_values (); @@ -468,7 +500,8 @@ let test_no_fingerprints _test_ctxt = assert_equal "" out ~pp_diff:print_string_diff; assert_equal "" err ~pp_diff:print_string_diff; assert_equal None exit_code; - assert_equal [`B ("no_fp", no_fp, true)] (changed_setting_values ()) ~pp_diff:print_setting_list_diff;; + assert_equal [`B ("no_fp", no_fp, true)] (changed_setting_values ()) ~pp_diff:print_setting_list_diff; + reset_setting_values ();; let test_no_fingerprints_between_lines _test_ctxt = reset_setting_values (); @@ -478,7 +511,8 @@ let test_no_fingerprints_between_lines _test_ctxt = assert_equal "" out ~pp_diff:print_string_diff; assert_equal "" err ~pp_diff:print_string_diff; assert_equal None exit_code; - assert_equal [`I ("nofp_sl", nofp_sl, expected_start); `I ("nofp_el", nofp_el, expected_end)] (changed_setting_values ()) ~pp_diff:print_setting_list_diff;; + assert_equal [`I ("nofp_sl", nofp_sl, expected_start); `I ("nofp_el", nofp_el, expected_end)] (changed_setting_values ()) ~pp_diff:print_setting_list_diff; + reset_setting_values ();; let test_clean_fingerprints _test_ctxt = reset_setting_values (); @@ -487,7 +521,8 @@ let test_clean_fingerprints _test_ctxt = assert_equal "" out ~pp_diff:print_string_diff; assert_equal "" err ~pp_diff:print_string_diff; assert_equal None exit_code; - assert_equal [`B ("cleanfp", cleanfp, true)] (changed_setting_values ()) ~pp_diff:print_setting_list_diff;; + assert_equal [`B ("cleanfp", cleanfp, true)] (changed_setting_values ()) ~pp_diff:print_setting_list_diff; + reset_setting_values ();; (* Cannot test --erasefp due to side-effects *) (* Cannot test --printfp due to side-effects *) @@ -500,7 +535,8 @@ let test_use_fingerprints _test_ctxt = assert_equal "" out ~pp_diff:print_string_diff; assert_equal "" err ~pp_diff:print_string_diff; assert_equal None exit_code; - assert_equal [`SO ("fpf_in", fpf_in, Some expected_fp_file)] (changed_setting_values ()) ~pp_diff:print_setting_list_diff;; + assert_equal [`SO ("fpf_in", fpf_in, Some expected_fp_file)] (changed_setting_values ()) ~pp_diff:print_setting_list_diff; + reset_setting_values ();; let test_fp_deb _test_ctxt = reset_setting_values (); @@ -509,7 +545,8 @@ let test_fp_deb _test_ctxt = assert_equal "" out ~pp_diff:print_string_diff; assert_equal "" err ~pp_diff:print_string_diff; assert_equal None exit_code; - assert_equal [`B ("fp_deb", fp_deb, true)] (changed_setting_values ()) ~pp_diff:print_setting_list_diff;; + assert_equal [`B ("fp_deb", fp_deb, true)] (changed_setting_values ()) ~pp_diff:print_setting_list_diff; + reset_setting_values ();; let test_cache_dir _test_ctxt = reset_setting_values (); @@ -519,7 +556,8 @@ let test_cache_dir _test_ctxt = assert_equal "" out ~pp_diff:print_string_diff; assert_equal "" err ~pp_diff:print_string_diff; assert_equal None exit_code; - assert_equal [`S ("cachedir", cachedir, expected_cache_dir)] (changed_setting_values ()) ~pp_diff:print_setting_list_diff;; + assert_equal [`S ("cachedir", cachedir, expected_cache_dir)] (changed_setting_values ()) ~pp_diff:print_setting_list_diff; + reset_setting_values ();; let cli_test_suite = "Test CLI Parsing" >::: [ "Help Test" >:: test_help; @@ -537,7 +575,7 @@ let cli_test_suite = "Test CLI Parsing" >::: [ "Isabelle/TLA+ Check Test" >:: test_use_isabelle_tla; "Max Threads Test" >:: test_set_max_threads; "Set Method Test" >:: test_set_method; - "Custom Solver Test" >:: test_set_solver; + (*"Custom Solver Test" >:: test_set_solver;*) "Custom SMT Logic Test" >:: test_set_smt_logic; "Stretch Test" >:: test_stretch; "No Flatten Test" >:: test_no_flatten; From 02f98f7b37be3f7f5fb5528860d0f9e9c74b93a8 Mon Sep 17 00:00:00 2001 From: Andrew Helwer Date: Fri, 28 Nov 2025 14:28:10 -0800 Subject: [PATCH 10/11] Prefer Format.fprintf to Format.pp_print_text Signed-off-by: Andrew Helwer --- src/params.ml | 2 +- src/tlapm_args.ml | 18 +++++++++--------- 2 files changed, 10 insertions(+), 10 deletions(-) diff --git a/src/params.ml b/src/params.ml index 56381cbd4..0894bdea6 100644 --- a/src/params.ml +++ b/src/params.ml @@ -131,7 +131,7 @@ let get_exec err e = else "." in let msg = msg1 ^ msg2 in - Format.pp_print_text err msg; + Format.fprintf err "%s" msg; e := NotFound msg; failwith msg; end; diff --git a/src/tlapm_args.ml b/src/tlapm_args.ml index 8969cd153..c872d6152 100644 --- a/src/tlapm_args.ml +++ b/src/tlapm_args.ml @@ -7,8 +7,7 @@ open Params let show_version formatter terminate = - Format.pp_print_text formatter (rawversion ()); - Format.pp_print_cut formatter (); + Format.fprintf formatter "%s\n" (rawversion ()); terminate 0 let set_debug_flags flgs = @@ -58,7 +57,7 @@ let parse_args executable_name args opts mods usage_fmt err terminate = Arg.parse_argv args opts (fun mfile -> mods := mfile :: !mods) (Printf.sprintf usage_fmt (Filename.basename executable_name)) with Arg.Bad msg -> - Format.pp_print_text err msg; + Format.fprintf err "%s\n" msg; terminate 2 let show_where out terminate = @@ -67,7 +66,7 @@ let show_where out terminate = Format.fprintf out "%s\n" path; terminate 0 | None -> - Format.pp_print_text out "N/A\n"; + Format.fprintf out "N/A\n"; terminate 1 let set_nofp_start s = @@ -246,20 +245,21 @@ let init ?(out=Format.std_formatter) ?(err=Format.err_formatter) ?(terminate=exi in helpfn := begin fun () -> Arg.usage_string opts - (Printf.sprintf usage_fmt (Filename.basename executable_name)) |> Format.pp_print_text err; + (Printf.sprintf usage_fmt (Filename.basename executable_name)) + |> Format.fprintf err "%s"; terminate 0 end ; parse_args executable_name args opts mods usage_fmt err terminate; if !show_config || !verbose then begin - Format.pp_print_text out (printconfig err true); - Format.pp_print_cut out (); + Format.fprintf out "%s\n" (printconfig err true); end ; if !show_config then terminate 0 ; if !mods = [] then begin Arg.usage_string opts (Printf.sprintf "Need at least one module file.\n\n\ Usage: %s FILE ...\noptions are:" - (Filename.basename executable_name)) |> Format.pp_print_text err; + (Filename.basename executable_name)) + |> Format.fprintf err "%s"; terminate 2 end ; if !summary then begin @@ -276,7 +276,7 @@ let init ?(out=Format.std_formatter) ?(err=Format.err_formatter) ?(terminate=exi tm.Unix.tm_hour tm.Unix.tm_min tm.Unix.tm_sec; Format.fprintf out " with command line:\n\\*"; Array.iter (fun s -> Format.fprintf out " %s" (quote_if_needed s)) args; - Format.pp_print_text out "\n\n%!" + Format.fprintf out "\n\n%!" end; if !use_stdin && (List.length !mods) <> 1 then begin Arg.usage opts From 39dc7be9185404470d95261276e88edfb81139bf Mon Sep 17 00:00:00 2001 From: Andrew Helwer Date: Thu, 18 Dec 2025 11:03:27 -0800 Subject: [PATCH 11/11] Responding to PR feedback Signed-off-by: Andrew Helwer --- src/tlapm_args.ml | 1 - src/tlapm_args.mli | 3 ++- test/cli/cli_tests.ml | 15 ++++++++------- 3 files changed, 10 insertions(+), 9 deletions(-) diff --git a/src/tlapm_args.ml b/src/tlapm_args.ml index c872d6152..63acc4a55 100644 --- a/src/tlapm_args.ml +++ b/src/tlapm_args.ml @@ -50,7 +50,6 @@ let set_default_method meth = with Failure msg -> raise (Arg.Bad ("--method: " ^ msg)) -(* FIXME use Arg.parse instead *) let parse_args executable_name args opts mods usage_fmt err terminate = try Arg.current := 0; diff --git a/src/tlapm_args.mli b/src/tlapm_args.mli index 6bde11eef..02add4069 100644 --- a/src/tlapm_args.mli +++ b/src/tlapm_args.mli @@ -6,6 +6,7 @@ Copyright (C) 2011 INRIA and Microsoft Corporation (** Given the executable name and an array of command-line arguments, parses those arguments then either sets associated values in the Params module or directly takes action such as printing out file contents or deleting - directories. Returns a list of files for proof checking. + directories. Returns a list of files for proof checking. The optional + arguments are used for unit tests. *) val init: ?out:Format.formatter -> ?err:Format.formatter -> ?terminate:(int -> unit) -> string -> string array -> string list diff --git a/test/cli/cli_tests.ml b/test/cli/cli_tests.ml index 6c70ab131..e33601e28 100644 --- a/test/cli/cli_tests.ml +++ b/test/cli/cli_tests.ml @@ -17,8 +17,10 @@ let capture_output (f : Format.formatter -> unit) : string = f out_format; Format.pp_print_flush out_format (); Buffer.contents out - +(** This function is a quick hack that is very inefficient; avoid using + it on large haystacks. +*) let rec string_contains (needle : string) (haystack : string) : bool = match haystack with | "" -> false @@ -68,7 +70,7 @@ let setting_value_changed (setting : setting_value) = | `F (_, rf, v) -> not (!rf = v) | `S (_, rf, v) -> not (!rf = v) | `SO (_, rf, v) -> not (!rf = v) - | `SL (_, rf, v) -> not (List.equal String.equal !rf v) + | `SL (_, rf, v) -> not (!rf = v) | `ML (_, rf, v) -> not (!rf = v) let changed_setting_value (setting : setting_value) = @@ -275,7 +277,7 @@ let test_search_paths _test_ctxt : unit = | [`SL ("rev_search_path", _, [_; first_path; second_path])] -> assert_bool "Should have first path" (string_contains "some/other/module/path" first_path); assert_bool "Should have second path" (string_contains "some/module/path" second_path); - | _ -> assert_bool "Search path not as expected" false; + | _ -> assert_bool "Search path not as expected" false; reset_setting_values ();; let test_keep_going _test_ctxt = @@ -329,7 +331,6 @@ let test_set_method _text_ctxt = assert_equal [`ML ("default_method", default_method, [Tlapm_lib__Method.Fail])] (changed_setting_values ()) ~pp_diff:print_setting_list_diff; reset_setting_values ();; -(* let test_set_solver _test_ctxt = reset_setting_values (); let solver_cmd = "my_solver_cmd" in @@ -342,7 +343,6 @@ let test_set_solver _test_ctxt = (* Params.exec is unfortunately an opaque type whose value we cannot directly access *) assert_bool "Solver command should be custom" (string_contains solver_cmd (solve_cmd smt "file.tla")); reset_setting_values ();; -*) let test_set_smt_logic _test_ctxt = reset_setting_values (); @@ -558,7 +558,7 @@ let test_cache_dir _test_ctxt = assert_equal None exit_code; assert_equal [`S ("cachedir", cachedir, expected_cache_dir)] (changed_setting_values ()) ~pp_diff:print_setting_list_diff; reset_setting_values ();; - + let cli_test_suite = "Test CLI Parsing" >::: [ "Help Test" >:: test_help; "Basic Test" >:: test_basic; @@ -575,7 +575,7 @@ let cli_test_suite = "Test CLI Parsing" >::: [ "Isabelle/TLA+ Check Test" >:: test_use_isabelle_tla; "Max Threads Test" >:: test_set_max_threads; "Set Method Test" >:: test_set_method; - (*"Custom Solver Test" >:: test_set_solver;*) + "Custom Solver Test" >:: test_set_solver; "Custom SMT Logic Test" >:: test_set_smt_logic; "Stretch Test" >:: test_stretch; "No Flatten Test" >:: test_no_flatten; @@ -599,3 +599,4 @@ let cli_test_suite = "Test CLI Parsing" >::: [ ];; let () = run_test_tt_main cli_test_suite +