installing why3 through opam
I have installed why
through opam
opam switch
# switch compiler description
4.07.1 ocaml-base-compiler.4.07.1 4.07.1
-> 4.07.1+flambda ocaml-variants.4.07.1+flambda 4.07.1+flambda
default ocaml-base-compiler.4.11.0 default
opam list
# Packages matching: installed
# Name # Installed # Synopsis
alt-ergo 2.3.3 The Alt-Ergo SMT prover
alt-ergo-lib 2.3.3 The Alt-Ergo SMT prover library
alt-ergo-parsers 2.3.3 The Alt-Ergo SMT prover parser library
...
ocaml 4.07.1 The OCaml compiler (virtual package)
...
why3 1.3.3 Why3 environment for deductive program verification
why3-coq 1.3.3 Why3 environment for deductive program verification
why3-ide 1.3.3 Why3 environment for deductive program verification
...
unfortunately when trying to run the example I got the following error message
why3 ide hello_proof.why
/usr/local/lib/why3/plugins/hypothesis_selection cannot be loaded: Dynlink error: cannot find file /usr/local/lib/why3/plugins/hypothesis_selection.cmxs in search path
/usr/local/lib/why3/plugins/tptp cannot be loaded: Dynlink error: cannot find file /usr/local/lib/why3/plugins/tptp.cmxs in search path
/usr/local/lib/why3/plugins/genequlin cannot be loaded: Dynlink error: cannot find file /usr/local/lib/why3/plugins/genequlin.cmxs in search path
Fatal error while loading driver file '/usr/local/share/why3/drivers/alt_ergo_0.94.drv':
anomaly: Sys_error("/usr/local/share/why3/drivers/alt_ergo_0.94.drv: No such file or directory")
I have nothing under /usr/local/lib/why3
and /usr/local/share/why3
. What did I do wrongg?