coq-club AT inria.fr

Subject: The Coq mailing list

List archive

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

From: e AT x80.org (Emilio Jesús Gallego Arias)
To: Benedikt Ahrens <benedikt.ahrens AT gmx.net>
Cc: coq-club AT inria.fr, Pierre Courtieu <pierre.courtieu AT gmail.com>, 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, 07 Dec 2017 22:07:35 +0100
Authentication-results: mail3-smtp-sop.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:zHNkZB1EPvFPzYXosmDT+DRfVm0co7zxezQtwd8ZsegWL/ad9pjvdHbS+e9qxAeQG96Eu7QZ06L/iOPJZy8p2d65qncMcZhBBVcuqP49uEgeOvODElDxN/XwbiY3T4xoXV5h+GynYwAOQJ6tL3WbmHC57CYTFxPjLkI1Y72tQs+Bx/iwgsq//ZDfYgZUzBO9e750N13ipwjXu8UXgpckI6Yrxx3SinRNa6JQyH8+dnyJmBOp6++grMYl9D5f87IM8s9EUKKyXakj36cQIz0iN20644XCrxjKVkrctTMnTmwKn08QUED+5xbgU8K063Oiuw==
Organization: X80 Heavy Industries

Benedikt Ahrens
<benedikt.ahrens AT gmx.net>
writes:

> 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?

- Use OCaml < 4.06.0?
- Or as pointed out before, change:

`let coq_safe_string = "-safe-string"`

to

`let coq_safe_string = ""`

in configure.ml

E.

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