Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] ocaml version required for coq 8.10.1

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] ocaml version required for coq 8.10.1


Chronological Thread 
  • From: Cao Qinxiang <caoqinxiang AT gmail.com>
  • To: coq-club AT inria.fr
  • Subject: Re: [Coq-Club] ocaml version required for coq 8.10.1
  • Date: Mon, 28 Oct 2019 20:25:27 +0800
  • Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=caoqinxiang AT gmail.com; spf=Pass smtp.mailfrom=caoqinxiang AT gmail.com; spf=None smtp.helo=postmaster AT mail-ot1-f54.google.com
  • Ironport-phdr: 9a23:/lKApxQkfWfzdwbxxbDi+5g3Btpsv+yvbD5Q0YIujvd0So/mwa69YBON2/xhgRfzUJnB7Loc0qyK6vumCD1LusbJmUtBWaQEbwUCh8QSkl5oK+++Imq/EsTXaTcnFt9JTl5v8iLzG0FUHMHjew+a+SXqvnYdFRrlKAV6OPn+FJLMgMSrzeCy/IDYbxlViDanbr5+MRu7oR/Vu8QSjodvJKU8wQbVr3VVfOhb2XlmLk+JkRbm4cew8p9j8yBOtP8k6sVNT6b0cbkmQLJBFDgpPHw768PttRnYUAuA/WAcXXkMkhpJGAfK8hf3VYrsvyTgt+p93C6aPdDqTb0xRD+v4btnRAPuhSwaMTMy7WPZhdFqjK9Drx2hqR5wzY7abo+WKfRwYL/ScMgASmZdRMtcTTBNDp++YoYJEuEPPfxYr474p1YWsxaxHw6sD/70xD9JgH/30qw63P4nEQHJwQctGM4Bv27TrNXsNacSV++0zKjSwjXFYPNbwjj96I3SfRAgpfGAR65/cc3UyUQ2EQ7Ok1ueqYvgPzyP1+QNtXCW4PZnVeK2l2Eosxp+ojmpxss2j4nJgoQYwU3H+yVh2Is5O8G0RUphbdOnEJZcrT+WO5ZqTs84Q2xltyA3waAct5GhZigF0pEnygbfa/OZd4iI5QruVOOLLjd5gHJpYbW/hwqv/US5xO3xVsa53ExFripCldnMuXQN2ALJ5sebTft9+1+t2TeJ1w/N9uFJOV44mbbfJpI7wbM9loAfvVreEiPqgkn7jKCbel0h+uey6uTnZrvmpoWbN49xkgzxLr4hmsumAeQ5NAgPUGmb9v661L3s5kD5T7BKgec3kqndqpzVOcMbpquhDw9Pzokj8wq/Dyuh0NkAgXYHK0tFdAubgIjtJlHBO+v1Dey/glSpiDdk3erKPrznApXXL3jMiq3tfbhn6x0U9A1mxtdGoplQF7spIfTpW0a3usaLIAU+NlmfyuGvMdR7xoIXX23HVqSQN7rTt0+J7+QgC+aJbY4R/j36Lq52tLbVkXYllApFLuGS1pwNZSXgR6g0EwCieXPpx+w5PyISpANnFb7ljVSDVXhYYHPgB/tttAF+M5qvCML4fq7ohbWA2CmhGZgPPzJJD1mNFTHjcIDWAq5ROhLXGddol3k/bZbkS4Il0kvz5grzyr4iKfaNvyNF6dTs09964+CVnhY3p2R5
Problems solved. 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



On Mon, Oct 28, 2019 at 6:06 PM Cao Qinxiang <caoqinxiang AT gmail.com> wrote:
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
>

Archive powered by MHonArc 2.6.18.

Top of Page