Should be possible to install without menhir about compcert HOT 2 CLOSED

The reason we need the latest Menhir version is actually not for cparser/Parser.{vy,v} (the Coq-verified parser) but for cparser/pre_parser.{mly,mli,.ml} (the "pre-parser" that is responsible for token disambiguation and error messages). The latest Menhir adds sophisticated support for reporting and explaining syntax errors, which the CompCert trunk takes great advantage.

Putting generated files in a Git repo is never a good thing to do. We did it for a while with cparser/Parser.v when Menhir's Coq output mode was brand new, but it caused much problems with merges and with the configure/Makefile logic.

For Linux and MacOS X, the OPAM package manager makes it extremely easy to get up-to-date versions of OCaml and Menhir. Install OPAM (http://opam.ocaml.org/doc/Install.html), then do opam switch 4.02.3 then opam install menhir, and you're done.

For MS Windows, the Cygwin packages for OCaml and Menhir are too old, so installation from sources is needed.

from compcert.

The AbsInt folks mention that their customers in the critical software industry frown on generated files being included in a source distribution. (It's not cricket with respect to certification procedures.) So, we decided not to include Menhir-generated files in the repository. Sorry for the inconvenience.

from compcert.