coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] [ANN] Raising the minimal OCaml version for Coq 8.10 to 4.05.0

From: Emilio Jesús Gallego Arias <e AT x80.org>
To: Théo Zimmermann <theo.zimmi AT gmail.com>
Cc: coq-club AT inria.fr
Subject: Re: [Coq-Club] [ANN] Raising the minimal OCaml version for Coq 8.10 to 4.05.0
Date: Sat, 22 Sep 2018 18:44:34 +0200
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=e AT x80.org; spf=Pass smtp.mailfrom=e AT x80.org; spf=Pass smtp.helo=postmaster AT x80.org
Ironport-phdr: 9a23:6dciAxCZnBATgKAXPmX9UyQJP3N1i/DPJgcQr6AfoPdwSPv6psbcNUDSrc9gkEXOFd2Cra4c1KyO6+jJYi8p2d65qncMcZhBBVcuqP49uEgeOvODElDxN/XwbiY3T4xoXV5h+GynYwAOQJ6tL1LdrWev4jEMBx7xKRR6JvjvGo7Vks+7y/2+94fcbglUhjexe69+IAmrpgjNq8cahpdvJLwswRXTuHtIfOpWxWJsJV2Nmhv3+9m98p1+/SlOovwt78FPX7n0cKQ+VrxYES8pM3sp683xtBnMVhWA630BWWgLiBVIAgzF7BbnXpfttybxq+Rw1DWGMcDwULs5Xymp4aV2Rx/ykCoJNyA3/nzQisx+gqxUohGvqBJwzIHIb4+YL+Z+frrHcN8GWWZMRMRcWipcCY28dYsPCO8BMP5XoYn4plsOqRq+BQ60C+3r1DBInWXu3bYi3OogCw7G2AggEMwBsHTTtNr4KL0SUeGvw6nT0D7OaO1Z1Czy6YXLbhwtu/aMXah/ccfIz0QkCgDLjk2IpID4PD6Y1f4Bv3aF4+dhT+6jlmwqpxxrrjSyyMoglJHFi4AXx1ze6Cl0zoc4Kce3RUN1e9KoDptduiGcOoBrWM0tWXtotzw/yrAeuZ60YiwKyJM/yh/QaPGLb5KE4hX5VOaeOTt4hXRld6yjhxuq7EStye7xWtOq3FpUrydJiMTAu3IQ2xDJ98SKROVx8l+k2TmV1gDT7u9EIVozlareM5Mu3KU9l5UQvEjfBCP2n1/2jKCOekU+5ueo8/jnYqnhppKEK4B0jRj+Pr0ylcy7HOQ3KRMDX3Ob+OS5zL3s51f1QLRMjv0sk6nWqorWJcoBpv3xPwgA7oai7F6NDjKj3c4dlH8BZAZZeB+AyZroPlTPCP/9BPa7xV+rlWE46erBO+jMB5TJL3/0srr6761KxEdYzAc8yud2/ZNdEflVLdrjChe3s8bXWExqezeoyvrqXY0unrgVXniCV/fAYfHi9GSQ7+dqGNGiIYocuTLzMf8gtqz+3Sd/nkUSL/DwgcknLUugF/EjGH23JGL2i4ZTATdS+A0kQ76y0QDQYXtof3+3GpkEyHQ7BYahXNXTFtjrh6aOjn62
Organization: X80 Heavy Industries

Théo Zimmermann
<theo.zimmi AT gmail.com>
writes:

> Emilio meant: at the time of the release of Coq 8.10, Debian Buster will be
> the new stable version and it contains indeed OCaml 4.05. Unfortunately,
> given that Debian doesn't announce clear release dates, it is not clear
> that Debian Buster will really be the new stable at the time of the release
> of Coq 8.10.

Indeed, that's what I mean. Debian has gotten better at releasing more
consistently, so indeed Coq 8.10 and Debian Buster should arrive close
enough.

Anyways, an important practical consideration is that Debian Buster
users should be able to get packages for Coq 8.10, 8.11, 8.12 without
too much trouble. [well, Coq is so outdated in Debian sid right now that
we should request its removal, but that's a different story]

> Side question: why do you recommend using the system compiler with OPAM?

Indeed, I tend to strongly recommend _against_ mixing OPAM and system
packages. I have seen a fair amount of issues in non-expert users due to
this configuration. Also, OPAM 2.0 may have changed in this regard.

E.

[Coq-Club] [ANN] Raising the minimal OCaml version for Coq 8.10 to 4.05.0, Emilio Jesús Gallego Arias, 09/19/2018
- Re: [Coq-Club] [ANN] Raising the minimal OCaml version for Coq 8.10 to 4.05.0, Ralf Jung, 09/22/2018
  - Re: [Coq-Club] [ANN] Raising the minimal OCaml version for Coq 8.10 to 4.05.0, Théo Zimmermann, 09/22/2018
    - Re: [Coq-Club] [ANN] Raising the minimal OCaml version for Coq 8.10 to 4.05.0, Emilio Jesús Gallego Arias, 09/22/2018
      - Re: [Coq-Club] [ANN] Raising the minimal OCaml version for Coq 8.10 to 4.05.0, Bernhard Schommer, 09/24/2018