coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] ocaml version required for coq 8.10.1

From: Cao Qinxiang <caoqinxiang AT gmail.com>
To: coq-club AT inria.fr
Subject: [Coq-Club] ocaml version required for coq 8.10.1
Date: Mon, 28 Oct 2019 17:04:43 +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-f52.google.com
Ironport-phdr: 9a23:dHp5pxzbw/KpGNzXCy+O+j09IxM/srCxBDY+r6Qd1OoQIJqq85mqBkHD//Il1AaPAdyAraMUwLOM7ejJYi8p2d65qncMcZhBBVcuqP49uEgeOvODElDxN/XwbiY3T4xoXV5h+GynYwAOQJ6tL1LdrWev4jEMBx7xKRR6JvjvGo7Vks+7y/2+94fcbglVijexe7d/IRa5oQnMqMUbgJZpJ7osxBfOvnZGYfldy3lyJVKUkRb858Ow84Bm/i9Npf8v9NNOXLvjcaggQrNWEDopM2Yu5M32rhbDVheA5mEdUmoNjBVFBRXO4QzgUZfwtiv6sfd92DWfMMbrQ704RSiu4qF2QxLulSwJNSM28HvPh8N/jKxVrhGvqQFhzYHIe4yaLuZyc7nHcN8GWWZMXMBcXDFBDIOmaIsPCvIMMPhCoIn6ulAAthq+BQ+jBePu0DBIgHD21rA93us9Cw7G2xUgH9MIsHXbrdX6LqESUe+uwanHyDXMdfJW2TPn5IfUdRAhpOiBULRtesTS0UkiDx3JgkmUpID/PD6Y1v4Bv3aG4+Z8T+6ii3ArpgdsqTa13MgskJPGhocNx1DE6yp5xIE1KMW9SEFhYN6kFIJctyaGN4drW88iTWFltDggxr0Jvp67eycKyJA5yBLFd/OHdI2I7griVOaXPzh4mGpodKyjixu260Stye3xWtOq3FpXsiZJiNnBum4V2xzW8MeHS/99/km72TaI0gDe8v1LLlozlarCKp4hxLExlpsJvkTFES/7g0r2jKqMeUUl/uik8fjoYrLjppOELY97lhn+Mrgymsy4Gek3Lg8OX3GC9eug0L3j4Fb2Ta5Rjvw2l6nZqIrVKd4apq6/GQ9V05ws5wyxDze8g5wkmiwMK0sAcxaahaDoPUvPKbb2F6SRmVOpxRxiwLj/P7vxA5zLITCXm77mZLd7+09VzgUbwtVW5pYSAbYEdqGgEnTtvcDVW0dqeze/xPzqXY0kitEuHFmXC6rcC5v89EeS77t2ceaJbY4R/j36Lqp9vq+8vToCgVYYOJKR894SYXG8EO5hJhzAM3Xpi9YFV2wNu1hnFbG4uBi5STdWIk2Kcec86zU8Ut/0CI7CQsWqnOXE0nrhWJJRYW9CBxaHFnK6L4g=

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

[Coq-Club] ocaml version required for coq 8.10.1, Cao Qinxiang, 10/28/2019
- Re: [Coq-Club] ocaml version required for coq 8.10.1, Gaëtan Gilbert, 10/28/2019
  - Re: [Coq-Club] ocaml version required for coq 8.10.1, Cao Qinxiang, 10/28/2019
    - Re: [Coq-Club] ocaml version required for coq 8.10.1, Cao Qinxiang, 10/28/2019