From 6fb8aa76d579304aa900c7cf80196a2cdfb2e3e4 Mon Sep 17 00:00:00 2001
From: Michele Alberti <michele.alberti@cea.fr>
Date: Thu, 17 Nov 2022 15:01:54 +0100
Subject: [PATCH] [cmdline] Format file specification is not needed for
verify-json command.
---
src/main.ml | 22 +++++++++++-----------
1 file changed, 11 insertions(+), 11 deletions(-)
diff --git a/src/main.ml b/src/main.ml
index 42ae008..843aa75 100644
--- a/src/main.ml
+++ b/src/main.ml
@@ -120,7 +120,7 @@ let timelimit_of_string s =
| [ v ], [ "h" ] -> Int.of_string v * 3600
| _ -> invalid_arg "Unrecognized time limit"
-let verify format loadpath memlimit timelimit prover dataset_csv files =
+let verify ?format loadpath ?memlimit ?timelimit prover dataset_csv files =
let debug = log_level_is_debug () in
let memlimit = Option.map memlimit ~f:memlimit_of_string in
let timelimit = Option.map timelimit ~f:timelimit_of_string in
@@ -130,7 +130,7 @@ let verify format loadpath memlimit timelimit prover dataset_csv files =
?dataset_csv)
files
-let verify_json format loadpath memlimit timelimit file =
+let verify_json loadpath ?memlimit ?timelimit file =
let json_config =
match
Verification.File.json_config_of_yojson (Yojson.Safe.from_file file)
@@ -154,7 +154,7 @@ let verify_json format loadpath memlimit timelimit file =
failwith
(Fmt.str "No '%s' file or directory" json_config.property.dataset)
in
- verify format loadpath memlimit timelimit json_config.prover dataset_csv
+ verify loadpath ?memlimit ?timelimit json_config.prover dataset_csv
[ Verification.File.of_json_config json_config ]
let exec_cmd cmdname cmd =
@@ -210,10 +210,6 @@ let timelimit =
Arg.(
value & opt (some string) None & info [ "t"; "timelimit" ] ~doc ~docv:"TIME")
-let format =
- let doc = "File format." in
- Arg.(value & opt (some string) None & info [ "format" ] ~doc)
-
let loadpath =
let doc = "Additional loadpath." in
Arg.(value & opt_all string [ "." ] & info [ "L"; "loadpath" ] ~doc)
@@ -226,6 +222,10 @@ let verify_cmd =
~doc
~man:[ `S Manpage.s_description; `P doc ]
in
+ let format =
+ let doc = "File format." in
+ Arg.(value & opt (some string) None & info [ "format" ] ~doc)
+ in
let term =
let files =
let doc = "File to verify." in
@@ -253,7 +253,7 @@ let verify_cmd =
const
(fun format loadpath memlimit timelimit prover dataset_csv files _ ->
exec_cmd cmdname (fun () ->
- verify format loadpath memlimit timelimit prover dataset_csv files))
+ verify ?format loadpath ?memlimit ?timelimit prover dataset_csv files))
$ format $ loadpath $ memlimit $ timelimit $ prover $ dataset_csv $ files
$ setup_logs)
in
@@ -277,10 +277,10 @@ let verify_json_cmd =
required & pos ~rev:true 0 (some file) None & info [] ~doc ~docv:"FILE")
in
Term.(
- const (fun format loadpath memlimit timelimit json _ ->
+ const (fun loadpath memlimit timelimit json _ ->
exec_cmd cmdname (fun () ->
- verify_json format loadpath memlimit timelimit json))
- $ format $ loadpath $ memlimit $ timelimit $ json $ setup_logs)
+ verify_json loadpath ?memlimit ?timelimit json))
+ $ loadpath $ memlimit $ timelimit $ json $ setup_logs)
in
Cmd.v info term
--
GitLab