diff --git a/caisar.opam b/caisar.opam
index 60de520366980053823117a77e434790f58254e7..8aecdaf27b5a888caa18b8146757936f04b40e96 100644
--- a/caisar.opam
+++ b/caisar.opam
@@ -21,7 +21,7 @@ depends: [
"dune" {>= "2.9" & >= "2.9.3"}
"base" {>= "v0.14.0"}
"stdio" {>= "v0.14.0"}
- "cmdliner" {= "1.0.4"}
+ "cmdliner" {= "1.1.1"}
"fmt" {>= "0.8.9"}
"logs" {>= "0.7.0"}
"ppx_deriving" {>= "5.1"}
diff --git a/dune-project b/dune-project
index 241ea49b7d16c8e4ebc1fcd5d4e828f79a02d6d6..a5f3e2ee3764d2c4dfe5bda42a51640a63b0a6c8 100644
--- a/dune-project
+++ b/dune-project
@@ -64,7 +64,7 @@
(dune (>= 2.9.3))
(base (>= v0.14.0))
(stdio (>= v0.14.0))
- (cmdliner (= 1.0.4))
+ (cmdliner (= 1.1.1))
(fmt (>= 0.8.9))
(logs (>= 0.7.0))
(ppx_deriving (>= 5.1))
diff --git a/src/main.ml b/src/main.ml
index 41e09fa8165c8a94f4ea7c1edd22bcd0eade67fe..f468f0899e23f238150a431c527db7b4f2e18c69 100644
--- a/src/main.ml
+++ b/src/main.ml
@@ -102,19 +102,23 @@ let exec_cmd cmdname cmd =
let config_cmd =
let cmdname = "config" in
- let detect =
- let doc = "Detect solvers in \\$PATH." in
- Arg.(value & flag & info [ "d"; "detect" ] ~doc)
- in
- let doc = Fmt.str "%s configuration." caisar in
- let exits = Term.default_exits in
- let man =
- [
- `S Manpage.s_description;
- `P (Fmt.str "Handle the configuration of %s." caisar);
- ]
+ let info =
+ let doc = Fmt.str "%s configuration." caisar in
+ let exits = Cmd.Exit.defaults in
+ let man =
+ [
+ `S Manpage.s_description;
+ `P (Fmt.str "Handle the configuration of %s." caisar);
+ ]
+ in
+ Cmd.info cmdname ~sdocs:Manpage.s_common_options ~exits ~doc ~man
in
- ( Term.(
+ let term =
+ let detect =
+ let doc = "Detect solvers in \\$PATH." in
+ Arg.(value & flag & info [ "d"; "detect" ] ~doc)
+ in
+ Term.(
ret
(const (fun detect _ ->
if not detect
@@ -123,56 +127,63 @@ let config_cmd =
(* TODO: Do not only check for [detect], and enable it by default,
as soon as other options are available. *)
`Ok (exec_cmd cmdname (fun () -> config true ())))
- $ detect $ setup_logs)),
- Term.info cmdname ~sdocs:Manpage.s_common_options ~exits ~doc ~man )
+ $ detect $ setup_logs))
+ in
+ Cmd.v info term
let verify_cmd =
let cmdname = "verify" in
- let files =
- let doc = "Files to verify." in
- let file_or_stdin = Verification.File.(of_string, pretty) in
- Arg.(value & pos_all file_or_stdin [] & info [] ~doc)
- in
- let format =
- let doc = "File format." in
- Arg.(value & opt (some string) None & info [ "format" ] ~doc)
- in
- let loadpath =
- let doc = "Additional loadpath." in
- Arg.(value & opt_all string [ "." ] & info [ "L"; "loadpath" ] ~doc)
- in
- let memlimit =
- let doc = "Memory limit (in megabytes)." in
- Arg.(value & opt (some int) None & info [ "m"; "memlimit" ] ~doc)
+ let doc =
+ "Property verification of neural networks using external provers."
in
- let timeout =
- let doc = "Timeout (in seconds)." in
- Arg.(value & opt (some int) None & info [ "t"; "timeout" ] ~doc)
+ let info =
+ Cmd.info cmdname ~sdocs:Manpage.s_common_options ~exits:Cmd.Exit.defaults
+ ~doc
+ ~man:[ `S Manpage.s_description; `P doc ]
in
- let prover =
- let all_provers = Prover.list_available () in
- let doc =
- Fmt.str
- "Prover to use. Support is provided for the following provers: %s."
- (Fmt.str "%a"
- (Fmt.list ~sep:Fmt.comma Fmt.string)
- (List.map ~f:Prover.to_string all_provers))
+ let term =
+ let files =
+ let doc = "Files to verify." in
+ let file_or_stdin = Verification.File.(of_string, pretty) in
+ Arg.(value & pos_all file_or_stdin [] & info [] ~doc)
in
- let provers =
- Arg.enum (List.map ~f:(fun p -> (Prover.to_string p, p)) all_provers)
+ let format =
+ let doc = "File format." in
+ Arg.(value & opt (some string) None & info [ "format" ] ~doc)
in
- Arg.(required & opt (some provers) None & info [ "p"; "prover" ] ~doc)
- in
- let dataset_csv =
- let doc = "Dataset under CSV format. Currently only supported by SAVer." in
- Arg.(value & opt (some file) None & info [ "dataset-csv" ] ~doc)
- in
- let doc =
- "Property verification of neural networks using external provers."
- in
- let exits = Term.default_exits in
- let man = [ `S Manpage.s_description; `P doc ] in
- ( Term.(
+ let loadpath =
+ let doc = "Additional loadpath." in
+ Arg.(value & opt_all string [ "." ] & info [ "L"; "loadpath" ] ~doc)
+ in
+ let memlimit =
+ let doc = "Memory limit (in megabytes)." in
+ Arg.(value & opt (some int) None & info [ "m"; "memlimit" ] ~doc)
+ in
+ let timeout =
+ let doc = "Timeout (in seconds)." in
+ Arg.(value & opt (some int) None & info [ "t"; "timeout" ] ~doc)
+ in
+ let prover =
+ let all_provers = Prover.list_available () in
+ let doc =
+ Fmt.str
+ "Prover to use. Support is provided for the following provers: %s."
+ (Fmt.str "%a"
+ (Fmt.list ~sep:Fmt.comma Fmt.string)
+ (List.map ~f:Prover.to_string all_provers))
+ in
+ let provers =
+ Arg.enum (List.map ~f:(fun p -> (Prover.to_string p, p)) all_provers)
+ in
+ Arg.(required & opt (some provers) None & info [ "p"; "prover" ] ~doc)
+ in
+ let dataset_csv =
+ let doc =
+ "Dataset under CSV format. Currently only supported by SAVer."
+ in
+ Arg.(value & opt (some file) None & info [ "dataset-csv" ] ~doc)
+ in
+ Term.(
ret
(const
(fun format loadpath memlimit timeout prover dataset_csv files _ ->
@@ -180,10 +191,11 @@ let verify_cmd =
(exec_cmd cmdname (fun () ->
verify format loadpath memlimit timeout prover dataset_csv files)))
$ format $ loadpath $ memlimit $ timeout $ prover $ dataset_csv $ files
- $ setup_logs)),
- Term.info cmdname ~sdocs:Manpage.s_common_options ~exits ~doc ~man )
+ $ setup_logs))
+ in
+ Cmd.v info term
-let default_cmd =
+let default_info =
let doc =
"A platform for characterizing the safety and robustness of artificial \
intelligence based software."
@@ -200,14 +212,14 @@ let default_cmd =
]
in
let version = "0.1" in
- ( Term.(ret (const (fun _ -> `Help (`Pager, None)) $ const ())),
- Term.info caisar ~version ~doc ~sdocs ~exits:Term.default_exits ~man )
+ let exits = Cmd.Exit.defaults in
+ Cmd.info caisar ~version ~doc ~sdocs ~exits ~man
+
+let default_cmd = Term.(ret (const (fun _ -> `Help (`Pager, None)) $ const ()))
let () =
- match
- Term.(eval_choice ~catch:false default_cmd [ config_cmd; verify_cmd ])
- with
- | `Error _ -> Caml.exit 1
- | _ -> Caml.exit (if Logs.err_count () > 0 then 1 else 0)
- | exception exn when not (log_level_is_debug ()) ->
+ try
+ Cmd.group ~default:default_cmd default_info [ config_cmd; verify_cmd ]
+ |> Cmd.eval ~catch:false |> Caml.exit
+ with exn when not (log_level_is_debug ()) ->
Fmt.epr "%a@." Why3.Exn_printer.exn_printer exn