coq-club AT inria.fr

Subject: The Coq mailing list

List archive

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

From: Gaëtan Gilbert <gaetan.gilbert AT skyskimmer.net>
To: coq-club AT inria.fr
Subject: Re: [Coq-Club] ocaml version required for coq 8.10.1
Date: Mon, 28 Oct 2019 10:08:05 +0100
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=gaetan.gilbert AT skyskimmer.net; spf=Pass smtp.mailfrom=gaetan.gilbert AT skyskimmer.net; spf=None smtp.helo=postmaster AT relay12.mail.gandi.net
Ironport-phdr: 9a23:jRdAohaTobglbQcm/ospyMP/LSx+4OfEezUN459isYplN5qZoMS6bnLW6fgltlLVR4KTs6sC17ON9fGxEUU7or+5+EgYd5JNUxJXwe43pCcHRPC/NEvgMfTxZDY7FskRHHVs/nW8LFQHUJ2mPw6arXK99yMdFQviPgRpOOv1BpTSj8Oq3Oyu5pHfeQpFiCezbL9oKBi7qRjau9ULj4dlNqs/0AbCrGFSe+RRy2NoJFaTkAj568yt4pNt8Dletuw4+cJYXqr0Y6o3TbpDDDQ7KG81/9HktQPCTQSU+HQRVHgdnwdSDAjE6BH6WYrxsjf/u+Fg1iSWIdH6QLYpUjmk8qxlSgLniD0fOjAk7m/XhMx+gqFVrh2vqBNwwZLbbo6OOfpifa7QZ88WSXZPU8tTUSFKH4Oyb5EID+oEJetWrpPyoEcSrRSkAwmjHOLhyj5MhnDtw6I6yfghGhzB0QwvBd0BrmjUo8/zNKsIXuC1za3Iwi7dYPNMxTfw85PIchMhoPGXXrJwcM/RyUwxGAPflFmQr5LqPy+M2+kLrmOV7PJgWPqxh2I6qQx9uDqiyts2hoXUhI8YyUrI+Tt3zYorPdG0VUB2bNG+HJdNsyyWLZZ6T8EmTm1ypSo3yb8LtJimdyYQ0psn3QTQa/mffoiI/B3jUOGRLC9ihH17fLKwnRaz/VW+xuHmU8m7yldKri5fntnDrH8N0QHc6smdRvt74EihxS6D1wHV6u5aPUA5jbTXJ4Mjz7IqlJcfrV7PEjL0lUj1lqOaaEsp9vaw5+TieLrmp5ucN4FuigH5N6QjgsO/Dv4mPQgSRWeb//6w1LLi/U39W7pFkOc2krXCvZDBJsQaprW5AwxU0oYm7hawES2m3M4enXYZMFJJYAiHgJTxO1HSPPD4Cu+yjEirkDdy3vzJIrnhAojWIXXYi7fgfbN961ZGxwYpzNBf4YhUCrAbL/7pVE/xro+QMhhsOAuthu3jFd9V14UEWGvJDLXKHrnVtAqn72EzKu+7S44RsjvnN7Bx6PfjkXY/31AceaOkx4c/c3OpBfdnJkCUezzqj8tXQjRChRY3UOG/0A7KajVUfXvnB/tttAF+M5qvCML4fq7ohbWA2CmhGZgPODJdCUGXEnbtcoieHfEBdHDLe5Mzonk/TbGkDrQZ+1S2rgajleh8LfvP+SwdsJ/5kt54+7+LzExgxXlPF82Yllq1YSR0k2cPHWNkxq17qF0kkBGG2Kl8xfNRE9BSofVETlViOA==

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

[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