Unbound value Why3.Whyconf.load_driver
Hi,
I'm trying to package frama-c 26.1
for the gentoo linux distribution.
Build must be done from source in a sandboxed directory and ideally should include system-wide dependencies, so I'm not using opam for fetching dependencies (which relies heavily on a home-directory configuration).
I managed to fix all errors so far but the following one:
File "src/plugins/wp/ProverWhy3.ml", line 1129, characters 12-36:
1129 | let drv = Why3.Whyconf.load_driver (Why3.Whyconf.get_main config)
^^^^^^^^^^^^^^^^^^^^^^^^
Error: Unbound value Why3.Whyconf.load_driver
The installed version of Why3 is 1.6.0 with gtk ocamlopt zarith zip
features enabled and coq doc emacs re sexp stackify
disabled (i.e. the standard selection for this package).
The meaning of these features is documented as follows:
- coq - Add sci-mathematics/coq support
- doc - Add extra documentation (API, Javadoc, etc). It is recommended to enable per package instead of globally
- emacs - Add support for GNU Emacs
- gtk - Build the IDE x11-libs/gtk+
- ocamlopt - Enable ocamlopt support (ocaml native code compiler) -- Produces faster programs (Warning: you have to disable/enable it at a global scale)
- re - Use Re (dev-ml/re) instead of Str for regular expressions
- sexp - Add support for outputting S-expressions with dev-ml/ppx_sexp_conv
- stackify - Enable structure reconstruction algorithm for MLCFG
- zarith - Use Zarith (dev-ml/zarith) instead of Nums (dev-ml/num) for computations
- zip - Enable compression of session files
Here is the ebuild file I came up with: frama-c-26.1.ebuild
Any tip on how to fix this last compilation error would be great.
Thanks a lot for your work and time.
-- Pierre-Nicolas