From 4835bd80eafb58ff6c3f724f108e8c4c1d2d472f Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Fran=C3=A7ois=20Bobot?= <francois.bobot@cea.fr>
Date: Mon, 11 Jul 2022 16:23:58 +0200
Subject: [PATCH] Use new autodetection API
---
caisar.opam | 5 +----
caisar.opam.template | 3 ---
dune-project | 2 +-
src/autodetect.ml | 15 +++++++++++++--
tests/marabou.t | 8 ++++----
tests/simple.t | 8 ++++----
tests/simple_onnx.t | 8 ++++----
tests/simple_ovo.t | 8 ++++----
8 files changed, 31 insertions(+), 26 deletions(-)
diff --git a/caisar.opam b/caisar.opam
index 81d04b88..60de5203 100644
--- a/caisar.opam
+++ b/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" ]
-]
diff --git a/caisar.opam.template b/caisar.opam.template
index 562220ac..e69de29b 100644
--- a/caisar.opam.template
+++ b/caisar.opam.template
@@ -1,3 +0,0 @@
-pin-depends: [
- [ "why3.1.4.0" "git+https://gitlab.inria.fr/why3/why3.git#047c34a8" ]
-]
diff --git a/dune-project b/dune-project
index 585375a4..241ea49b 100644
--- a/dune-project
+++ b/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))
diff --git a/src/autodetect.ml b/src/autodetect.ml
index 3f98d684..a7f5c262 100644
--- a/src/autodetect.ml
+++ b/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
diff --git a/tests/marabou.t b/tests/marabou.t
index dc2070d6..263f8682 100644
--- a/tests/marabou.t
+++ b/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.
diff --git a/tests/simple.t b/tests/simple.t
index 55a2088c..0b826992 100644
--- a/tests/simple.t
+++ b/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.
diff --git a/tests/simple_onnx.t b/tests/simple_onnx.t
index b947d7d2..600f9c82 100644
--- a/tests/simple_onnx.t
+++ b/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.
diff --git a/tests/simple_ovo.t b/tests/simple_ovo.t
index 42e51aea..9225ad73 100644
--- a/tests/simple_ovo.t
+++ b/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.
--
GitLab