GitLab

Menhir 20151112 can, in fact, be used to compile Why3. The actual issue
was that the error reporting module depends on Menhir's table-based
backend, which requires menhirLib. So, the latter is no longer an optional
dependency.

The standard install location of the num library is $OCAMLLIB. Thus, the
answer of ocamlfind cannot generally be trusted since it returns the
location of the META file. Yet, on Arch Linux, nums.cma is actually stored
next to its META file, for some reason. So, this commit makes configure
try this location before falling back to the standard one.

Generated statements were actually ill-formed, since Coq 8.4 sometimes
interprets "A -> B <-> C" as "(A -> B) <-> C". (This bug was fixed in 8.5.)
We could print additional parentheses to work around the issue, but it is
about time we drop support for Coq 8.4 anyway.

On Debian, .cmi files might be missing, while META files are installed.
This confuses ocamlfind in believing development files are available.
So, we now systematically check that there is at least a .cmi file.
This also helps when ocamlfind is not present.

On Debian, .cmi files might be missing, while META files are installed.
This confuses ocamlfind in believing development files are available.
So, we now systematically check that there is at least a .cmi file.
This also helps when ocamlfind is not present.

Why3 now looks for a %l/{coq,pvs}/version file to check which version of a
prover was used to compile realizations. In particular, there is no longer
any Config.compile_time_support variable set once and for all.

generated again.

* Makefile.in
Realizations for isabelle are generated even if Isabelle is not installed.
The .thy file are checked only if isabelle is installed. This allows us
to treat it as with coq and be able to detect changes in realizations
with a script.
Dont erase xml generated file during clean.

* configure.in
Changed the configure to always generate a default isabelle version (set
to 2017) for generation of the realization driver (needed even when no
isablle support is given).

* examples/regtests.sh
Adding option --check-realization and --only-realization which add a test
the compares the output of the new realization compared to the one
recorded. It complains if they are different forcing the user to update the
realization files.

* lib/isabelle/*
Adding xml files corresponding to generated realization for Isabelle. This
allows for the abovementionned script to work even if Isabelle is not
installed (which is the case for most people editing theories).

* examples/nightly-bench.sh
Add the option for realization check

* misc/ci-bench
Calls the test for realization

Conflicts:
	examples/regtests.sh

It is needed for compiling the Coq tactic Why3.vo file when native
compilation is disabled.

This commit also avoid a potential race condition when Why3.vo was
compiled with both the native and bytecode compilers.

Older versions of menhir fail to compile rules mixing inlined definitions
(e.g. ioption) with unnamed arguments (e.g. $2).

While they are aliases, ocamlfind behaves as if the latter was just
js_of_ocaml for the sake of querying (unless recursive), so the missing
package was not properly detected.