coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Coq 8.6 and Ocaml 4.06

From: Benedikt Ahrens <benedikt.ahrens AT gmx.net>
To: coq-club AT inria.fr, Pierre Courtieu <pierre.courtieu AT gmail.com>
Cc: Gabriel Scherer <gabriel.scherer AT gmail.com>, Benedikt Ahrens <benedikt.ahrens AT gmail.com>
Subject: Re: [Coq-Club] Coq 8.6 and Ocaml 4.06
Date: Thu, 7 Dec 2017 18:00:45 +0000
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=benedikt.ahrens AT gmx.net; spf=Pass smtp.mailfrom=benedikt.ahrens AT gmx.net; spf=None smtp.helo=postmaster AT mout.gmx.net
Ironport-phdr: 9a23:n+VEHx2+4YKXYMNSsmDT+DRfVm0co7zxezQtwd8ZsegUI/ad9pjvdHbS+e9qxAeQG96Eu7QZ06L/iOPJZy8p2d65qncMcZhBBVcuqP49uEgeOvODElDxN/XwbiY3T4xoXV5h+GynYwAOQJ6tL3WbmHC57CYTFxPjLkI1Y72tQs+Bx/iwguu14tjYZxhCrDu7e7J7ahus6U3pt8QMm4YqAaEs0AfIr2YAL/xXyHlyKBSYmAvm+sa94bZs9i1Rv7Qq8MsWAovgeKFtZ7FeATgnMHx9zc3xuB/YBV+F630RXmQVjlxBAxLI6grSUZLh9C33qrwui2GhIcTqQOVsCnyZ5KBxRUqt0X9fOg==

People keep stumbling over this issue of not being able to compile Coq 8.6 (and hence UniMath) with Ocaml 4.06.
I suspect that it will get worse in the next few days with the upcoming School on Univalent Mathematics.

Is there a simple fix that (i) could be pushed to the 8.6 branch soon (by Sunday 10 Dec) or (ii) could be applied locally?

On 11/23/2017 04:55 PM, Pierre Courtieu wrote:

Calling it 8.6.2 would indeed be misleading, but isn't a
"compiler-compatibility" release necessary anyway?

Best
Pierre

2017-11-23 17:28 GMT+01:00 Théo Zimmermann
<theo.zimmi AT gmail.com>:

Indeed. Releasing a 8.6.2 would make no sense because this branch has not
been maintained so it would send a wrong signal, but there is a v8.6 branch
that would be ready to receive a patch making it compile with OCaml 4.06 (I
prefer the lighter solution BTW). Even older branches like v8.5 could
receive such a patch.

Re: [Coq-Club] Coq 8.6 and Ocaml 4.06, Benedikt Ahrens, 12/07/2017
- Re: [Coq-Club] Coq 8.6 and Ocaml 4.06, Emilio Jesús Gallego Arias, 12/07/2017
  - Re: [Coq-Club] Coq 8.6 and Ocaml 4.06, Emilio Jesús Gallego Arias, 12/07/2017
- Re: [Coq-Club] Coq 8.6 and Ocaml 4.06, Maxime Dénès, 12/09/2017