CODEWITHSUNDEEP
ocamlcoqconfigure
OrenIshShalom
OrenIshShalom

Reputation: 7112

Building Coq from source fails with incorrect ocaml version

I'm trying to build Coq from source with:

$ git clone https://github.com/coq/coq.git
$ cd coq && ./configure

for which I get the (false) response:

Your version of OCaml is 4.04.0.
You need OCaml 4.05.0 or later.
Configuration script failed!

When I type ocaml --version in terminal here is what I get:

The OCaml toplevel, version 4.09.0+dev0-2019-01-18

So what's going on? who's right?

Upvotes: 1

Views: 93

Answers (1)

Jose Fernando Lopez Fernandez
Jose Fernando Lopez Fernandez

Reputation: 1159

Judging by the dev version number on the Ocaml binary, I'm guessing you probably built it yourself. If you remembered to do both make and make install, the binary will be in your /usr/local/bin directory, provided you didn't customize anything during the configuration. That directory is not in your path because it would be a nightmare for every release-build binary on your system to try to use your dev builds.

To build Coq, when you configure the package you need to pass in the directory where the Ocaml compiler you want to use is. So for example if you were using a test build of gcc you would do:

./configure CC=/usr/local/bin/gcc-8.2.1-testbuild .

Or something to that effect. To see what you have to do specifically here, you can do this:

./configure --help

You should then see an overview of what flags are relevant and whatnot. When a project depends on a package, as is the case here, the help menu should at least point you in the right direction.

Before I go, I will note that out of desperation, some people will flat out copy the new binary and replace the one in their /usr/bin directory. I can't recommend enough that you do not get into the habit of doing that. Once you start hopping over the guardrails that are in place for the preservation of your own sanity, it's only a matter of time before things hit the fan, and remember: the only thing worse than spending all night trying to get a package to work is spending all night trying to get all your packages to work.

Upvotes: 3

Related Questions