Merge branch 'fix/michele/fixups' into 'master'

Fix SAVer detection, and other minor fixups

See merge request laiser/caisar!26

config/caisar-detection-data.conf

@@ -55,7 +55,7 @@ use_at_auto_level = 1
 [ATP saver]
 name = "SAVer"
 exec = "saver"
-version_switch = "--version 2>&1 | cat"
+version_switch = "--version 2>&1 | head -n1 && (which saver > /dev/null 2>&1)"
 version_regexp = "\\(v[0-9.]+\\)"
 version_ok = "v1.0"
 command = "%e %{svm} %{dataset} %{abstraction} %{distance} %{epsilon}"

src/main.ml

@@ -78,11 +78,13 @@ let config detect () =
     in
     let open Why3 in
     let provers = Whyconf.get_provers config in
-    Logs.app (fun m ->
-      m "@[<v>%a@]"
-        (Pp.print_iter2 Whyconf.Mprover.iter Pp.newline Pp.nothing
-           Whyconf.print_prover Pp.nothing)
-        provers))
+    if not (Whyconf.Mprover.is_empty provers)
+    then
+      Logs.app (fun m ->
+        m "@[<v>%a@]"
+          (Pp.print_iter2 Whyconf.Mprover.iter Pp.newline Pp.nothing
+             Whyconf.print_prover Pp.nothing)
+          provers))
 
 let verify format loadpath memlimit timeout prover dataset_csv files =
   let debug = log_level_is_debug () in
@@ -100,20 +102,8 @@ let exec_cmd cmdname cmd =
 
 let config_cmd =
   let cmdname = "config" in
-  let dirvar = "DIR" in
-  let envs =
-    [
-      Term.env_info
-        ~doc:
-          "Absolute path to the directory containing the executable of a \
-           solver."
-        dirvar;
-    ]
-  in
   let detect =
-    let doc =
-      Fmt.str "Detect solvers in \\$PATH (or \\$%s, if specified)." dirvar
-    in
+    let doc = "Detect solvers in \\$PATH." in
     Arg.(value & flag & info [ "d"; "detect" ] ~doc)
   in
   let doc = Fmt.str "%s configuration." caisar in
@@ -134,7 +124,7 @@ let config_cmd =
                 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 ~envs ~exits ~doc ~man )
+    Term.info cmdname ~sdocs:Manpage.s_common_options ~exits ~doc ~man )
 
 let verify_cmd =
   let cmdname = "verify" in
@@ -162,7 +152,8 @@ let verify_cmd =
   let prover =
     let all_provers = Prover.list_available () in
     let doc =
-      Fmt.str "Prover to use. Available provers are: %s."
+      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))

tests/marabou.t

@@ -38,8 +38,8 @@ Test verify
   <autodetect>Generating strategies:
   <autodetect>Run: (Marabou --version) > $TMPFILE 2>&1
   <autodetect>Run: (alt-ergo --version) > $TMPFILE 2>&1
+  <autodetect>Run: (saver --version 2>&1 | head -n1 && (which saver > /dev/null 2>&1)) > $TMPFILE 2>&1
   <autodetect>Run: (pyrat.py --version) > $TMPFILE 2>&1
-  <autodetect>Run: (saver --version 2>&1 | cat) > $TMPFILE 2>&1
   <autodetect>Found prover Alt-Ergo version 2.4.0, OK.
   <autodetect>Found prover Marabou version 1.0.+, OK.
   <autodetect>Found prover PyRAT version 1.1, OK.

tests/simple.t

@@ -41,8 +41,8 @@ Test verify
   <autodetect>Generating strategies:
   <autodetect>Run: (Marabou --version) > $TMPFILE 2>&1
   <autodetect>Run: (alt-ergo --version) > $TMPFILE 2>&1
+  <autodetect>Run: (saver --version 2>&1 | head -n1 && (which saver > /dev/null 2>&1)) > $TMPFILE 2>&1
   <autodetect>Run: (pyrat.py --version) > $TMPFILE 2>&1
-  <autodetect>Run: (saver --version 2>&1 | cat) > $TMPFILE 2>&1
   <autodetect>Found prover Alt-Ergo version 2.4.0, OK.
   <autodetect>Found prover Marabou version 1.0.+, OK.
   <autodetect>Found prover PyRAT version 1.1, OK.

tests/simple_onnx.t

@@ -33,8 +33,8 @@ Test verify
   <autodetect>Generating strategies:
   <autodetect>Run: (Marabou --version) > $TMPFILE 2>&1
   <autodetect>Run: (alt-ergo --version) > $TMPFILE 2>&1
+  <autodetect>Run: (saver --version 2>&1 | head -n1 && (which saver > /dev/null 2>&1)) > $TMPFILE 2>&1
   <autodetect>Run: (pyrat.py --version) > $TMPFILE 2>&1
-  <autodetect>Run: (saver --version 2>&1 | cat) > $TMPFILE 2>&1
   <autodetect>Found prover Alt-Ergo version 2.4.0, OK.
   <autodetect>Found prover Marabou version 1.0.+, OK.
   <autodetect>Found prover PyRAT version 1.1, OK.

tests/simple_ovo.t

@@ -39,8 +39,8 @@ Test verify
   <autodetect>Generating strategies:
   <autodetect>Run: (Marabou --version) > $TMPFILE 2>&1
   <autodetect>Run: (alt-ergo --version) > $TMPFILE 2>&1
+  <autodetect>Run: (saver --version 2>&1 | head -n1 && (which saver > /dev/null 2>&1)) > $TMPFILE 2>&1
   <autodetect>Run: (pyrat.py --version) > $TMPFILE 2>&1
-  <autodetect>Run: (saver --version 2>&1 | cat) > $TMPFILE 2>&1
   <autodetect>Found prover Alt-Ergo version 2.4.0, OK.
   <autodetect>Found prover Marabou version 1.0.+, OK.
   <autodetect>Found prover PyRAT version 1.1, OK.