Make the GUI and the realizations compilable against an installed version of Why3
This would require some kind of --disable-why3-core
configuration option.
For the GUI, it would cause the build system to not depend on the local why3.cma
library but on the one found by ocamlfind query why3
. Modifying the INCLUDES
and EXTLIBS
environment variables should be sufficient.
For the realizations, it would mean getting rid of the Config.compile_time_support
symbol and replacing it with a more dynamic method. For example, why3 config
could look for a text file in the lib/why3/lib/coq
directory, which would indicate which versions of Why3 and Coq were used to compile the .vo
files.
Ideally, this would make it possible to no longer have some why3-base
and why3
Opam packages, but instead to have some why3
, why3-ide
, and why3-coq
Coq packages with meaningful dependencies.