5

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
Charlie Parker
  • 5,884
  • 57
  • 198
  • 323
  • crossposted: https://www.quora.com/unanswered/How-does-one-install-tcoq – Charlie Parker Dec 26 '18 at 01:12
  • I am not sure tcoq is going to be very useful for you, what are you trying to do? – ejgallego Dec 27 '18 at 08:53
  • Anyways you should install campl5 and in `configure` be sure that the picked tools are coming from the same OPAM install. The problem you have is likely due to having OCaml installed twice. – ejgallego Dec 27 '18 at 08:53
  • @ejgallego how do I make sure I only have 1 OCaml installed? How is that producing the issue and how do I fix it? – Charlie Parker Dec 28 '18 at 00:22
  • how do I make sure I have `campl5 ` or install it? brew install didn't work. – Charlie Parker Dec 28 '18 at 00:27
  • See the output of Coq's configure to understand why it is using different versions of the compiler. Likely you have a kind of a botched install. – ejgallego Dec 28 '18 at 02:23
  • @ejgallego btw, why do you think `tcoq` won't be very useful for me? – Charlie Parker Dec 28 '18 at 18:26
  • It is a research prototype; there are more mature tools that can do most of what it does [not everything tho] What are you trying to do? – ejgallego Dec 29 '18 at 00:26
  • @ejgallego does it have a python interface for ML to use for research? – Charlie Parker Dec 29 '18 at 00:28
  • A python interface for Coq could mean many things; what is the interface your are thinking of? For example SerAPI does not have a python interface, but an agnostic one; depending on your exact needs using it from Python would range from trivial to quite tricky. – ejgallego Dec 31 '18 at 00:00
  • @ejgallego what is SerAPI? I was having in mind the Gamepad link paper I put in the question. Is that not good? Or what did you have in mind/use? – Charlie Parker Dec 31 '18 at 22:33
  • 1
    SerAPI is a Coq toplevel that allows you to query for a lot of info about proof documents. May be useful for you. – ejgallego Jan 02 '19 at 18:03
  • @ejgallego your tool doesn't look bad at all. Though, it seems gamepad allows kernel level and mid level proof terms that might be useful to feed into my AI agents. But I might try SerAPI too though. I need to keep exploring/playing around with the available tools. – Charlie Parker Jan 29 '19 at 01:33
  • SerAPI can output kernel terms and glob_expr fine too if you need them. In fact, it provides faithful output, even tho it may not matters so much as you'll have to elaborate to features anyways – ejgallego Jan 29 '19 at 04:37

1 Answers1

5

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.

J-M. Gorius
  • 606
  • 4
  • 15
  • doesn't let me uninstall `camlp5`! :O because Coq needs it. Will add the error msg to the question: `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` – Charlie Parker Dec 28 '18 at 18:24
  • You can safely execute `brew uninstall --ignore-dependencies camlp5`, as `opam`will provide `camlp5` afterwards. – J-M. Gorius Dec 28 '18 at 20:48