diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml index 8fe240f9e137d9a95cd9a51302cea8ff7042f172..f5dbfc4508bb95718a118d7552b01b5aa7b600d9 100644 --- a/.gitlab-ci.yml +++ b/.gitlab-ci.yml @@ -3,13 +3,13 @@ stages: tests: stage: test - image: ocaml/opam@sha256:108b775e7bda2c6d3bddae61c9cdb003e40de746baf3a994e8f7b82d8301dd0a + image: ocaml/opam@sha256:013a26ccbaa8344b63274e335e2492c432cec1c3526b9ba888ab151abb2b4c25 cache: key: $CI_COMMIT_REF_SLUG paths: - _opam script: - - if [ ! -d _opam ]; then echo "no local switch in the CI cache, we setup a new switch"; opam switch create --yes --no-install . ocaml-base-compiler.4.11.1; fi + - if [ ! -d _opam ]; then echo "no local switch in the CI cache, we setup a new switch"; opam switch create --yes --no-install . ocaml-base-compiler.4.13.1; fi - eval $(opam env) - sudo apt-get update - sudo apt install -y protobuf-compiler diff --git a/caisar.opam b/caisar.opam index 04f8e424d3b5f7d920482b6ac14e88b70f5d102d..a472d8d330c713cb0e9127f749a16fb998e0ff18 100644 --- a/caisar.opam +++ b/caisar.opam @@ -3,7 +3,7 @@ opam-version: "2.0" version: "0.1" synopsis: "Framework for neural network verification" depends: [ - "ocaml" {>= "4.10"} + "ocaml" {>= "4.13.0"} "dune-site" {>= "2.9.0"} "piqi" {>= "0.7.6"} "piqilib" {>= "0.6.14"} diff --git a/dune-project b/dune-project index 1792e8746af599944bad3faf7cdf165f1dd89a40..e059691fc41a0b1493359e469096b799f58d0fe3 100644 --- a/dune-project +++ b/dune-project @@ -13,7 +13,7 @@ (name caisar) (synopsis "Framework for neural network verification") (depends - (ocaml (>= 4.10)) + (ocaml (>= 4.13.0)) (dune-site (>= 2.9.0)) (piqi (>= 0.7.6)) (piqilib (>= 0.6.14)) diff --git a/src/main.ml b/src/main.ml index 9a9b01a8bf3bbd410846a66dfcccf4127ddc394d..bc097c4ed001ee8cfdf86707ce1dbe6101996d74 100644 --- a/src/main.ml +++ b/src/main.ml @@ -127,7 +127,7 @@ let verify_cmd = in let loadpath = let doc = "Additional loadpath." in - Arg.(value & opt_all string [] & info [ "L" ] ~doc) + Arg.(value & opt_all string [ "." ] & info [ "L"; "loadpath" ] ~doc) in let memlimit = let doc = "Memory limit (in megabytes)." in diff --git a/src/verification.ml b/src/verification.ml index ee4d1ded5ab445aa8c960bf672bc03b03897367c..8a6539c13aa7eb2e28958a18821ee5eb7df11705 100644 --- a/src/verification.ml +++ b/src/verification.ml @@ -54,8 +54,8 @@ let call_prover ~limit config (prover : Why3.Whyconf.config_prover) driver task | Some _ -> assert false (* By construction of the meta. *) | None -> invalid_arg (Fmt.str "No neural network model found in task") in - let nn_file = Filename.concat (Caml.Sys.getcwd ()) nn_file in - let command = Re.replace_string nnet_or_onnx ~by:nn_file command in + let nn_file = Unix.realpath nn_file in + let command = Re__Core.replace_string nnet_or_onnx ~by:nn_file command in let call_prover_on_task task_prepared = let prover_call = Driver.prove_task_prepared ~libdir:(Whyconf.libdir config)