Rework and prepare cmdline to accept new command.

src/main.ml

@@ -158,7 +158,7 @@ let config_cmd =
       ret
         (const (fun detect _ ->
            if not detect
-           then `Help (`Pager, Some "config")
+           then `Help (`Pager, Some cmdname)
            else
              (* TODO: Do not only check for [detect], and enable it by default,
                 as soon as other options are available. *)
@@ -167,47 +167,43 @@ let config_cmd =
   in
   Cmd.v info term
 
+let memlimit =
+  let doc =
+    "Memory limit. $(docv) is intended in megabytes (MB) by default, but \
+     gigabytes (GB) and terabytes (TB) may also be specified instead."
+  in
+  Arg.(
+    value & opt (some string) None & info [ "m"; "memlimit" ] ~doc ~docv:"MEM")
+
+let timelimit =
+  let doc =
+    "Time limit. $(docv) is intended in seconds (s) by default, but minutes \
+     (m) and hours (h) may also be specified instead."
+  in
+  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)
+
 let verify_cmd =
   let cmdname = "verify" in
-  let doc = "Property verification using external provers." in
   let info =
+    let doc = "Property verification using external provers." in
     Cmd.info cmdname ~sdocs:Manpage.s_common_options ~exits:Cmd.Exit.defaults
       ~doc
       ~man:[ `S Manpage.s_description; `P doc ]
   in
   let term =
     let files =
-      let doc = "Files to verify." in
+      let doc = "File 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. $(docv) is intended in megabytes (MB) by default, but \
-         gigabytes (GB) and terabytes (TB) may also be specified instead."
-      in
-      Arg.(
-        value
-        & opt (some string) None
-        & info [ "m"; "memlimit" ] ~doc ~docv:"MEM")
-    in
-    let timelimit =
-      let doc =
-        "Time limit. $(docv) is intended in seconds (s) by default, but \
-         minutes (m) and hours (h) may also be specified instead."
-      in
-      Arg.(
-        value
-        & opt (some string) None
-        & info [ "t"; "timelimit" ] ~doc ~docv:"TIME")
+      Arg.(non_empty & pos_all file_or_stdin [] & info [] ~doc ~docv:"FILE")
     in
     let prover =
       let all_provers = Prover.list_available () in
@@ -227,15 +223,12 @@ let verify_cmd =
       Arg.(value & opt (some file) None & info [ "dataset-csv" ] ~doc)
     in
     Term.(
-      ret
-        (const
-           (fun format loadpath memlimit timelimit prover dataset_csv files _ ->
-           `Ok
-             (exec_cmd cmdname (fun () ->
-                verify format loadpath memlimit timelimit prover dataset_csv
-                  files)))
-        $ format $ loadpath $ memlimit $ timelimit $ prover $ dataset_csv
-        $ files $ setup_logs))
+      const
+        (fun format loadpath memlimit timelimit prover dataset_csv files _ ->
+        exec_cmd cmdname (fun () ->
+          verify format loadpath memlimit timelimit prover dataset_csv files))
+      $ format $ loadpath $ memlimit $ timelimit $ prover $ dataset_csv $ files
+      $ setup_logs)
   in
   Cmd.v info term