[new release] caisar (3.0)

[caisar-platform]

CHANGES:

• [prover] Add support for operators Transpose, Flatten, Reshape, and Gemm in the transformation from ONNX to SMTLIB.

• [packaging] Add a Nix environment for CAISAR. Nix is a package manager aiming for reproduceability. It is now possible to install CAISAR with a single command. The installation process through Nix is detailed in the documentation.

• [docker] convert the docker image to use the Nix environment.

• [prover] refine the integration of AIMOS

[mseri]

Tests are failing in the lower bounds test with

#=== ERROR while compiling caisar.3.0 =========================================#
# context              2.3.0 | linux/x86_64 | ocaml-base-compiler.5.3.0 | pinned(https://git.frama-c.com/api/v4/projects/1082/packages/generic/caisar/3.0/caisar-3.0.tbz)
# path                 ~/.opam/5.3/.opam-switch/build/caisar.3.0
# command              ~/.opam/opam-init/hooks/sandbox.sh build dune build -p caisar -j 31 --promote-install-files=false @install
# exit-code            1
# env-file             ~/.opam/log/caisar-7-5db3c5.env
# output-file          ~/.opam/log/caisar-7-5db3c5.out
### output ###
# File "lib/ovo/tests/dune", line 1, characters 0-0:
# Error: Module "Poly" is used in several stanzas:
# - lib/ovo/tests/dune:1
# - lib/ovo/tests/dune:16
# To fix this error, you must specify an explicit "modules" field in every
# library, executable, and executables stanzas in this dune file. Note that
# each module cannot appear in more than one "modules" field - it must belong
# to a single library or executable.

Do you know what may be causing it?

[mseri]

I think it may be enough to replace the two exectutable stanzas in lib/ovo/tests/dune
with

(executable
 (name linear)
 (modules linear)
 (libraries caisar.ovo caisar.onnx))

(executable
 (name poly)
 (modules poly)
 (libraries caisar.ovo caisar.onnx))

[caisar-platform]

I think it may be enough to replace the two exectutable stanzas in lib/ovo/tests/dune with

(executable
 (name linear)
 (modules linear)
 (libraries caisar.ovo caisar.onnx))

(executable
 (name poly)
 (modules poly)
 (libraries caisar.ovo caisar.onnx))

We will adress this. Also, we noticed a failure on archlinux builds, which we cannot find the root cause yet. We also realized that the opam file did not yield the good version number, so we will fix this.