Skip to content
Snippets Groups Projects
Commit 587de126 authored by Michele Alberti's avatar Michele Alberti
Browse files

Update cmdliner version.

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