Skip to Content.
Sympa Menu

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

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

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


Chronological Thread 
  • From: Théo Zimmermann <theo.zimmi AT gmail.com>
  • To: Gabriel Scherer <gabriel.scherer AT gmail.com>
  • Cc: Coq Club <coq-club AT inria.fr>, Benedikt Ahrens <benedikt.ahrens AT gmail.com>
  • Subject: Re: [Coq-Club] Coq 8.6 and Ocaml 4.06
  • Date: Thu, 23 Nov 2017 16:28:30 +0000
  • Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=theo.zimmi AT gmail.com; spf=Pass smtp.mailfrom=theo.zimmi AT gmail.com; spf=None smtp.helo=postmaster AT mail-ua0-f172.google.com
  • Ironport-phdr: 9a23:g9JIJxPb/YkufCJFtTYl6mtUPXoX/o7sNwtQ0KIMzox0KPz8rarrMEGX3/hxlliBBdydsK0UzbeO+4nbGkU+or+5+EgYd5JNUxJXwe43pCcHRPC/NEvgMfTxZDY7FskRHHVs/nW8LFQHUJ2mPw6aijSI4DUTAhTyMxZubqSwQ9aKzpf/6+fn1JTZeQRFgHKGarN/Nhis5VHev8MMgIZmbL06yhbTr2FgdOFfxGcuLlWWyUXS/MC1qaJjciNnifMk8sNaVKz8eexsUbxVC3I0MmUw5eXksBDCSU2E4X5KATZeqQZBHwWQtEKyZZz2qCav87MlgCQ=

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.

Le jeu. 23 nov. 2017 à 17:10, Gabriel Scherer <gabriel.scherer AT gmail.com> a écrit :
Yes, and it will remain forever convenient to be able to test old Coq
versions under newer OCaml releases. So at least having a 8.6
maintenance branch with either changes (which does not necessitate a
new release) would be very nice.

On Thu, Nov 23, 2017 at 4:51 PM, Emilio Jesús Gallego Arias <e AT x80.org> wrote:
> Théo Zimmermann <theo.zimmi AT gmail.com> writes:
>
>> Indeed, Coq is known to have issues with OCaml 4.06. The Opam packages
>> should be fixed to reflect this.
>
>> There is no plan to ever do a 8.6.2 release and 8.7.0 also has issues with
>> OCaml 4.06 (only concerns CoqIDE IIRC). Coq 8.7.1 is planned to be released
>> in December with OCaml 4.06 support.
>
> That being said, it is easy to add support for 4.06.0 in an eventual
> 8.6.2. We can either:
>
> - modify configure.ml:coq_safe_string so coq is not compiled with safe_string
> - backport the 8.7 changes [should be safe enough]
>
> E.



Archive powered by MHonArc 2.6.18.

Top of Page