Coq 8.9.1, and apparently previous versions too, do not compile with ocaml 4.08.0.
They fail with errors of the form:
- CAMLP5O plugins/ssrmatching/g_ssrmatching.ml4
- Error while loading “/Users/garrigue/.opam/4.08.0/lib/camlp5/pr_dump.cmo”: The module `Pr_dump’ is already loaded (either by the main program or a previously-dynlinked library).
Apparently, the coq Makefile.build wrongly asks camlp5o to load pr_dump.cmo, while it is already included.
However, until 4.07.1 this worked, so I suppose the behavior was more laxist.
I proposed PRs for Coq (rocq-prover/rocq#10650) and opam (ocaml/opam-repository#14668), but the problem is extensive, so a fix in ocaml might be simpler.
The problem was only discovered late because coq was waiting for the porting of camlp5, which happened just before 4.08.1.