Use new autodetection API

caisar.opam

@@ -29,7 +29,7 @@ depends: [
   "menhirLib" {>= "20210310"}
   "ppx_deriving_yojson" {>= "3.6.1"}
   "csv" {>= "2.4"}
-  "why3" {= "1.4.0"}
+  "why3" {>= "1.5.0"}
   "re"
   "caisar-nnet" {= version}
   "caisar-ovo" {= version}
@@ -53,6 +53,3 @@ build: [
   ["dune" "install" "-p" name "--create-install-files" name]
 ]
 dev-repo: "git+https://git.frama-c.com/pub/caisar.git"
-pin-depends: [
-  [ "why3.1.4.0" "git+https://gitlab.inria.fr/why3/why3.git#047c34a8" ]
-]

caisar.opam.template

-pin-depends: [
-  [ "why3.1.4.0" "git+https://gitlab.inria.fr/why3/why3.git#047c34a8" ]
-]

dune-project

@@ -72,7 +72,7 @@
    (menhirLib (>= 20210310))
    (ppx_deriving_yojson (>= 3.6.1))
    (csv (>= 2.4))
-   (why3 (= 1.4.0))
+   (why3 (>= 1.5.0))
    re
    (caisar-nnet (= :version))
    (caisar-ovo (= :version))

src/autodetect.ml

@@ -38,7 +38,18 @@ let autodetection ?(debug = false) () =
     lookup_file Dirs.Sites.config "caisar-detection-data.conf"
   in
   let data = Autodetection.Prover_autodetection_data.from_file caisar_conf in
+  let provers = Autodetection.find_provers data in
+  let provers =
+    List.fold_left ~init:[] provers ~f:(fun acc (path, name, version) ->
+      {
+        Autodetection.Partial.name;
+        path;
+        version;
+        shortcut = None;
+        manual = false;
+      }
+      :: acc)
+  in
   let config = Whyconf.init_config (Some null) in
-  let binaries = Autodetection.request_binaries_version config data in
-  let provers = Autodetection.compute_builtin_prover binaries config data in
+  let provers = Autodetection.compute_builtin_prover provers config data in
   Whyconf.set_provers config provers

tests/marabou.t

@@ -34,12 +34,12 @@ Test verify
   >      ((0.0:t) .< y1 \/ (0.5:t) .< y1) /\ (0.0:t) .< y2 .< (0.5:t)
   > end
   > EOF
+  <autodetect>Run: ($TESTCASE_ROOT/bin/pyrat.py --version) > $TMPFILE 2>&1
+  <autodetect>Run: ($TESTCASE_ROOT/bin/saver --version 2>&1 | head -n1 && (which saver > /dev/null 2>&1)) > $TMPFILE 2>&1
+  <autodetect>Run: ($TESTCASE_ROOT/bin/alt-ergo --version) > $TMPFILE 2>&1
+  <autodetect>Run: ($TESTCASE_ROOT/bin/Marabou --version) > $TMPFILE 2>&1
   <autodetect>0 prover(s) added
   <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>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

@@ -37,12 +37,12 @@ Test verify
   >      ((0.0:t) .< y1 \/ (0.5:t) .< y1) /\ (0.0:t) .< y2 .< (0.5:t)
   > end
   > EOF
+  <autodetect>Run: ($TESTCASE_ROOT/bin/pyrat.py --version) > $TMPFILE 2>&1
+  <autodetect>Run: ($TESTCASE_ROOT/bin/saver --version 2>&1 | head -n1 && (which saver > /dev/null 2>&1)) > $TMPFILE 2>&1
+  <autodetect>Run: ($TESTCASE_ROOT/bin/alt-ergo --version) > $TMPFILE 2>&1
+  <autodetect>Run: ($TESTCASE_ROOT/bin/Marabou --version) > $TMPFILE 2>&1
   <autodetect>0 prover(s) added
   <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>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

@@ -29,12 +29,12 @@ Test verify
   >      (0.0:t) .< y1 .< (0.5:t)
   > end
   > EOF
+  <autodetect>Run: ($TESTCASE_ROOT/bin/pyrat.py --version) > $TMPFILE 2>&1
+  <autodetect>Run: ($TESTCASE_ROOT/bin/saver --version 2>&1 | head -n1 && (which saver > /dev/null 2>&1)) > $TMPFILE 2>&1
+  <autodetect>Run: ($TESTCASE_ROOT/bin/alt-ergo --version) > $TMPFILE 2>&1
+  <autodetect>Run: ($TESTCASE_ROOT/bin/Marabou --version) > $TMPFILE 2>&1
   <autodetect>0 prover(s) added
   <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>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

@@ -35,12 +35,12 @@ Test verify
   >      robust_to svm_apply a (8.0:t)
   > end
   > EOF
+  <autodetect>Run: ($TESTCASE_ROOT/bin/pyrat.py --version) > $TMPFILE 2>&1
+  <autodetect>Run: ($TESTCASE_ROOT/bin/saver --version 2>&1 | head -n1 && (which saver > /dev/null 2>&1)) > $TMPFILE 2>&1
+  <autodetect>Run: ($TESTCASE_ROOT/bin/alt-ergo --version) > $TMPFILE 2>&1
+  <autodetect>Run: ($TESTCASE_ROOT/bin/Marabou --version) > $TMPFILE 2>&1
   <autodetect>0 prover(s) added
   <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>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.