OCaml and preprocessor have incompatible versions error when installing tcoq

Question

I was trying to install tcoq and I had the following error:

"/Users/pinocchio/.opam/4.05.0/bin/ocamlfind" ocamlc -rectypes  -w -3-52-56 -c grammar/compat5.ml
OCAMLC -c -pp grammar/gramCompat.mlp
>> Fatal error: OCaml and preprocessor have incompatible versions
Fatal error: exception Misc.Fatal_error
make[1]: *** [grammar/gramCompat.cmo] Error 2
make: *** [submake] Error 2

does someone know:

1. What the error means?
2. How to fix it?

I saw related post online:

https://coq-club.inria.narkive.com/h4i0KOH0/problem-compiling-coq

but it wasn't terribly helpful. I did:

ocaml -I +camlp5

as they suggested and it seems to be working fine...

I did do make clean but that didn't help.

---

I just realized I skipped step 3 of the INSTALL but idk if its related to the issue or what Im suppose to do with it:

3- The uncompression and un-tarring of the distribution file gave birth
   to a directory named "coq-8.xx". You can rename this directory and put
   it wherever you want. Just keep in mind that you will need some spare
   space during the compilation (reckon on about 300 Mb of disk space
   for the whole system in native-code compilation). Once installed, the
   binaries take about 30 Mb, and the library about 200 Mb.

---

I am trying to install gamepad and to do it one needs to follow instructions. In particular I ran the following 3 commands:

opam switch 4.05.0
opam install camlp4
opam install ocamlfind

---

Most current error:

make
/Library/Developer/CommandLineTools/usr/bin/make --warn-undefined-variable --no-builtin-rules -f Makefile.build
OCAMLC -c -pp grammar/gramCompat.mlp
>> Fatal error: OCaml and preprocessor have incompatible versions
Fatal error: exception Misc.Fatal_error
make[1]: *** [grammar/gramCompat.cmo] Error 2
make: *** [submake] Error 2

after reading that error it miraculously occurred to me to print the version of both ocaml and camlp5:

$ camlp5 -v
Camlp5 version 7.07 (ocaml 4.07.0)

and:

ocaml
    OCaml version 4.05.0

so obviously thats wrong, so perhaps first step is to fix camlp5 to work with 4.05.0 since thats the one I need.

---

I tried uninstalling camlp5 but it refused!

brew uninstall camlp5
Error: Refusing to uninstall /usr/local/Cellar/camlp5/7.07
because it is required by coq, which is currently installed.
You can override this and force removal with:
  brew uninstall --ignore-dependencies camlp5

Answer 1

It seems you already figured out what the error means. The version of OCaml to which your local camlp5 executable is targeted at differs from the OCaml version you are using through opam. Let me switch (pun intended) directly to the second part of your question.

The main problem here comes from the fact that you are using two different sources for OCaml packages, namely your package manager (e.g. brew) and opam. In order to fix your issue, you should install those packages from only one source. I would recommend opam, as it allows you to easily manage differenct OCaml versions through switches.

Simply uninstall your local version of camlp5 using, for example,

brew uninstall camlp5

then install it using opam:

opam install camlp5

This advice also applies to other OCaml packages like ocamlbuild, camlp4, etc.