"configure" warning desirable for menhir/ocaml mismatch

[andrew-appel]

This should be an easy scripting change in the "configure" file:

Suppose I have the correct up-to-date version of menhir already installed for building CompCert, but my installation of ocaml is more recent than the ocaml that I (had previously) used to build menhir. Then at the very end of the CompCert build-and-extract process, I get an error message that the menhir libraries use a different version of ocaml than the one that CompCert was compiled with, and the build fails.

It would be better to check for this mismatch in the configure script.

I only make this suggestion because this has happened to me twice now.

[bschommer]

I don't really know if the configure script is the right place for such a check and I don't want to complicate it more by adding more checks. How about using opam for keeping track that the menhir library uses the same version of ocaml as the one used for compiling CompCert?

[xavierleroy]

I'm not even sure how we could check this compatibility in the configure script, save by compiling a small Menhir-based test project...

@bschommer is right, OPAM is a good solution to those kinds of problems, and is the recommended way to prepare a build environment for CompCert (see chapter 2 of the user's manual).

Unless it offends someone, I move to close this issue.

[xavierleroy]

OK, we've agreed to close this issue.