diff --git a/.ocamlformat b/.ocamlformat index 602451fa17e13f4715bac4db2e9403b55fa2449c..42aaaea17fd5f6381117dac8f4943d6c393112b8 100644 --- a/.ocamlformat +++ b/.ocamlformat @@ -1,4 +1,4 @@ -version=0.20.1 +version=0.22.4 exp-grouping=parens if-then-else=keyword-first max-indent=2 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/config/dune b/config/dune index fd50a8bc2938e6591c4eadcfabe13f5281899ad9..4398e3dca7dcf0af0c46d0b0923bce5182889c8c 100644 --- a/config/dune +++ b/config/dune @@ -1,8 +1,10 @@ (install - (section (site (caisar config))) - (files caisar-detection-data.conf - (drivers/pyrat.drv as drivers/pyrat.drv) - (drivers/marabou.drv as drivers/marabou.drv) - (drivers/saver.drv as drivers/saver.drv) - ) -(package caisar)) + (section + (site + (caisar config))) + (files + caisar-detection-data.conf + (drivers/pyrat.drv as drivers/pyrat.drv) + (drivers/marabou.drv as drivers/marabou.drv) + (drivers/saver.drv as drivers/saver.drv)) + (package caisar)) 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/lib/nnet/dune b/lib/nnet/dune index 78df3604bfeb0dc9f446c94830734467a33770d1..6674a9ec4282b70f92cbd6da799fd90ac915ddd0 100644 --- a/lib/nnet/dune +++ b/lib/nnet/dune @@ -1,6 +1,5 @@ (library - (name nnet) - (public_name caisar-nnet) - (libraries base csv) - (synopsis "NNet parser for CAISAR") -) + (name nnet) + (public_name caisar-nnet) + (libraries base csv) + (synopsis "NNet parser for CAISAR")) diff --git a/lib/onnx/dune b/lib/onnx/dune index 707eb2ddacf480fc55451b333b8d44b9f06b1e56..1008baf43c6b2f5790fbed38985ca6e9e364c3ca 100644 --- a/lib/onnx/dune +++ b/lib/onnx/dune @@ -1,12 +1,11 @@ (library - (name onnx) - (public_name caisar-onnx) - (libraries base stdio ocaml-protoc-plugin) - (synopsis "ONNX parser for CAISAR") -) + (name onnx) + (public_name caisar-onnx) + (libraries base stdio ocaml-protoc-plugin) + (synopsis "ONNX parser for CAISAR")) (rule - (deps onnx_protoc.proto generate_onnx_interface.sh) - (targets onnx_protoc.ml) - (action (run ./generate_onnx_interface.sh)) -) + (deps onnx_protoc.proto generate_onnx_interface.sh) + (targets onnx_protoc.ml) + (action + (run ./generate_onnx_interface.sh))) diff --git a/lib/ovo/dune b/lib/ovo/dune index 919b62e475c9bbe60e42e3fb2ed194d83de0916e..65525220415adc6ac4b107ec54f4e06f9d701e2d 100644 --- a/lib/ovo/dune +++ b/lib/ovo/dune @@ -1,6 +1,5 @@ (library - (name ovo) - (public_name caisar-ovo) - (libraries base csv) - (synopsis "OVO parser for CAISAR") -) + (name ovo) + (public_name caisar-ovo) + (libraries base csv) + (synopsis "OVO parser for CAISAR")) diff --git a/src/dune b/src/dune index 2a6a24748525a3921081dcc7ebc06042d5fffe67..16397dcccc24f73f2946c29373a9cfeae4f9ff68 100644 --- a/src/dune +++ b/src/dune @@ -1,13 +1,34 @@ (executable - (name main) - (public_name caisar) - (libraries menhirLib yojson cmdliner logs logs.cli logs.fmt fmt.tty base unix str ppx_deriving_yojson.runtime nnet onnx ovo why3 dune-site re) - (preprocess (pps ppx_deriving_yojson ppx_deriving.show ppx_deriving.ord ppx_deriving.eq)) - (package caisar) -) + (name main) + (public_name caisar) + (libraries + menhirLib + yojson + cmdliner + logs + logs.cli + logs.fmt + fmt.tty + base + unix + str + ppx_deriving_yojson.runtime + nnet + onnx + ovo + why3 + dune-site + re) + (preprocess + (pps + ppx_deriving_yojson + ppx_deriving.show + ppx_deriving.ord + ppx_deriving.eq)) + (package caisar)) (include_subdirs unqualified) (generate_sites_module - (module dirs) - (sites caisar)) + (module dirs) + (sites caisar)) diff --git a/src/main.ml b/src/main.ml index 41e09fa8165c8a94f4ea7c1edd22bcd0eade67fe..53efcc8fd38cba1b0c77f26e4d48713125c7d326 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,61 @@ 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) - in - let timeout = - let doc = "Timeout (in seconds)." in - Arg.(value & opt (some int) None & info [ "t"; "timeout" ] ~doc) + let doc = "Property verification using external provers." in + 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 +189,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 +210,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 diff --git a/stdlib/dune b/stdlib/dune index ddb41974d6913934cd4b012521419b823e292ccd..f1d9fa74d11b355d516bcd7fd324e1b30e3242b1 100644 --- a/stdlib/dune +++ b/stdlib/dune @@ -1,4 +1,6 @@ (install - (section (site (caisar stdlib))) + (section + (site + (caisar stdlib))) (files caisar.mlw) -(package caisar)) + (package caisar)) diff --git a/tests/dune b/tests/dune index a99e393b5197ae909350dfe66d9f66ba56ed5dba..9e2e5eafc3f263f1bf4bde94d54cc9a0cdd9599b 100644 --- a/tests/dune +++ b/tests/dune @@ -1,12 +1,10 @@ (cram - (deps - (package caisar) - TestNetwork.nnet - TestNetworkONNX.onnx - TestSVM.ovo - bin/pyrat.py - bin/Marabou - bin/saver - ) + (deps (package caisar) -) + TestNetwork.nnet + TestNetworkONNX.onnx + TestSVM.ovo + bin/pyrat.py + bin/Marabou + bin/saver) + (package caisar))