coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Coq with OCaml-4.08.0

From: Gaëtan Gilbert <gaetan.gilbert AT skyskimmer.net>
To: coq-club AT inria.fr
Subject: Re: [Coq-Club] Coq with OCaml-4.08.0
Date: Mon, 24 Jun 2019 11:45:18 +0200
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 relay4-d.mail.gandi.net
Ironport-phdr: 9a23:DXC3IRUkMKCaVDES+lO4ftygQFnV8LGtZVwlr6E/grcLSJyIuqrYbBaAt8tkgFKBZ4jH8fUM07OQ7/m6HzVaqs/e+DBaKdoQDkZD0Z1X1yUbQ+e9QXXhK/DrayFoVO9jb3RCu0+BDE5OBczlbEfTqHDhpRQbGxH4KBYnbr+tQt2agMu4zf299IPOaAtUmjW9falyLBKrpgnNq8Uam4RvJrsvxhfTv3dEZetayX5qKFmOmxrw+tq88IRs/ihNpv4t7dJMXbn/c68lUbFWETMqPnwv6sb2rxfDVwyP5nUdUmUSjBVFBhXO4Q/5UJnsrCb0r/Jx1yaGM8L4S7A0Qimi4LxwSBD0kicHNiU2/3/Rh8dtka9UuhOhpxh4w47JfIGYMed1c63Bcd8GQ2dKQ8BcXDFDDIyhdYsCF/cPM/hWr4f9pFUAoxWxCgauC+zzxTFFnWP20K4g3ug9DQ3L0g4tEtQTu3rUttX1M6ISXPi0wqbS0TLDc+lZ2THl54bJcxAhpeqDUqxqccrN1EIiEAzFgU+Opoz5JTyV0P4Bs2ea7+pkTu2glXQnqx1qrzi0xcctipLJhoEUylDB8CV23pw1Kce+SEFlfd6pCZ1dvDyZOYtuWs4uXXxktSQgxrAEpZK3ZjUGxZcpyhLFdvCKd4mF7gr+WOufLjp0nm9pdbalixqv80WtzvfwWtS13VtEqCdOj8PCuWoX1xPJ78iKUvt98Vml2TaIzw3T8P9LIUQumqvbJJMt26M/moAWsUvZHy/2nF/6jKCMeUUi5+eo6v7rYrP4qZ+AL4N0iwf+PboymsGnH+g0LwoDU3KZ9OigzrHv4E70TbtQgvErlqTUsYjWJcEBqa64Bw9V3Jwj6xG6Dzq+39QXh2cILE5fdxKBlYTpNFDOIPTjAvihmVSsjCxmx+vFPrzhGZXNLXnDkLLkfblj8U5Q0gwzws5D555MELEOPOrzWlPttNzfFhI2Lwu0w//+BNph0oMeRHmAD7SCMKLStF+I/vggL/ONZI8Tojb9KuIq6+TgjX8jyhchevyi2oJSY3SlFNxnJV+YaDzimIQvC2AP6yU3z/DjjmqtUDpZamyuF/Yz7zwnAYTgAobHTI23nJSa3zagHZxTY21cTFaBDSG7JM2/R/4QZXfKcYdamTseWO35Et5z5VSVrAb/joFfAK/R8ywcu4jk0YErtfbQhAox9DlxAt7b1WyRHTgtwjE4AgQu1aU6mnRTj0+Z2PEm0edbBMdQ5vZMXx18M5PAnbQjVoLCHznZd9LMc26IB9WrBTZrE4ArztsHcho4F5OnhxHHmSWjBbMU0bqGGM5s/w==

We can also wait until Coq 8.10 which doesn't use camlp5 ;)

Gaëtan Gilbert

On 24/06/2019 08:06, Xuanrui Qi wrote:

It seems that we will have to wait until camlp5 supports 4.08.0.

Xuanrui

On Sun, 2019-06-23 at 19:59 +1000, mukesh tiwari wrote:

I just updated my OCaml compiler, but I can't install the coq. I am
wondering if there would be Coq version for OCaml-4.08.0.

keep-learnings-MacBook-Pro:CoqUtility keep_learning$ opam list
# Packages matching: installed
# Name # Installed # Synopsis
base-bigarray base
base-threads base
base-unix base
ocaml 4.08.0 The OCaml compiler (virtual package)
ocaml-base-compiler 4.08.0 Official release 4.08.0
ocaml-config 1 OCaml Switch Configuration
keep-learnings-MacBook-Pro:CoqUtility keep_learning$ opam install coq
The following dependencies couldn't be met:
- coq → camlp5 → ocaml < 4.08.0
base of this switch (use `--unlock-base' to force)
- coq → ocaml < 4.06.0
base of this switch (use `--unlock-base' to force)

No solution found, exiting

Best,
Mukesh

[Coq-Club] Coq with OCaml-4.08.0, mukesh tiwari, 06/23/2019
- Re: [Coq-Club] Coq with OCaml-4.08.0, Xuanrui Qi, 06/24/2019
  - Re: [Coq-Club] Coq with OCaml-4.08.0, Gaëtan Gilbert, 06/24/2019
    - Re: [Coq-Club] Coq with OCaml-4.08.0, Vincent Laporte, 06/24/2019
      - Re: [Coq-Club] Coq with OCaml-4.08.0, Gaëtan Gilbert, 06/24/2019
      - Re: [Coq-Club] Coq with OCaml-4.08.0, Emilio Jesús Gallego Arias, 06/24/2019