The Coq mailing list

[Cao Qinxiang <caoqinxiang AT gmail.com>]

Aha. Yes, it said 4.02.3. I just need to fix that. Thank you very much!

BTW, now I have the following lines in the end when I "make world" for Coq (if I install ocaml-bytecode):

File "topbin/coqc_bin.ml", line 1:

Error: The file /usr/local/lib/ocaml/nums.cma is not a bytecode object file

make[1]: *** [bin/coqc.byte] Error 2

make: *** [submake] Error 2

Or the following if I install ocaml native-code:

COQMKTOP -o bin/coqc.opt

File "topbin/coqc_bin.ml", line 1:

Error: The file /usr/local/lib/ocaml/nums.cmxa is not a compilation unit description

make[1]: *** [bin/coqc.opt] Error 2

make: *** [submake] Error 2

I am trying to fix this. But any quick solutions? Thanks a lot!

Qinxiang Cao

Shanghai Jiao Tong University, John Hopcroft Center

Room 1110-2, SJTUSE Building

800 Dongchuan Road, Shanghai, China, 200240

On Mon, Oct 28, 2019 at 5:08 PM Gaëtan Gilbert <gaetan.gilbert AT skyskimmer.net> wrote:

What does "ocamlfind ocamlc -version" say?

Gaëtan Gilbert

On 28/10/2019 10:04, Cao Qinxiang wrote:
> Dear Coq clubbers,
>
> I try to compile Coq 8.10.1 from source code today. It requires ocaml
> 4.05.0 or later. I had ocaml 4.02.3 previously and build ocaml 4.09.0
> from source code today (make world + sudo make install).
>
> Now, if I "./configure" in coq 8.10.1 source code folder, I still get:
>
>     Your version of OCaml is 4.02.3.
>
>     You need OCaml 4.05.0 or later.
>
>     Configuration script failed!
>
>
> But "ocamlc -v" gives me:
>
>     The OCaml compiler, version 4.09.0
>
>     Standard library directory: /usr/local/lib/ocaml
>
>
> Do you have any idea how should I fix this? Thank you very much!
>
> Best,
> Qinxiang Cao
> Shanghai Jiao Tong University, John Hopcroft Center
> Room 1110-2, SJTUSE Building
> 800 Dongchuan Road, Shanghai, China, 200240
>