coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Coq 8.6 and Ocaml 4.06

From: John Leo <leo AT halfaya.org>
To: coq-club AT inria.fr
Cc: Benedikt Ahrens <benedikt.ahrens AT gmail.com>
Subject: [Coq-Club] Coq 8.6 and Ocaml 4.06
Date: Wed, 22 Nov 2017 16:13:45 -0800
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=leo AT halfaya.org; spf=None smtp.mailfrom=leo AT halfaya.org; spf=None smtp.helo=postmaster AT mail-it0-f47.google.com
Ironport-phdr: 9a23:mE6wrBU6iFpzh+YHtx+utE2YmJvV8LGtZVwlr6E/grcLSJyIuqrYZRKOt8tkgFKBZ4jH8fUM07OQ6P+wHzFYqb+681k8M7V0HycfjssXmwFySOWkMmbcaMDQUiohAc5ZX0Vk9XzoeWJcGcL5ekGA6ibqtW1aMlzFOAF0PuX4HJLJx4Tyjrjqus6bXwIdjz2kJLh2MR+erAPLt8BQj5ExBLw2z07rpXtOM8Bbwis8IV+Utxb14sm57Zcl9D5f7aFyv/VcWLn3KvxrBYdTCy4rZiVsvJXm

Hello everyone,

I'm new to this list so I apologize if this has been asked before. I recently tried to install UniMath using Ocaml 4.06; UniMath depends on Coq 8.6.1 which fails to compile with Ocaml 4.06 due to the change in behavior with bytes/string. I don't see any information online about 8.6.1 not working with 4.06; this page implies it does:

https://opam.ocaml.org/packages/coq/coq.8.6.1/

My question then is if there is an easy way UniMath (which uses 8.6.1 as a submodule) could get 8.6.1 to compile with Ocaml 4.06. Also will 8.6.2 support 4.06 and when is that due to be released? Finally does Coq 8.7.0 support Ocaml 4.06?

Thanks very much.

John Leo

[Coq-Club] Coq 8.6 and Ocaml 4.06, John Leo, 11/23/2017
- Re: [Coq-Club] Coq 8.6 and Ocaml 4.06, Théo Zimmermann, 11/23/2017
  - Re: [Coq-Club] Coq 8.6 and Ocaml 4.06, Emilio Jesús Gallego Arias, 11/23/2017
    - Re: [Coq-Club] Coq 8.6 and Ocaml 4.06, Gabriel Scherer, 11/23/2017
      - Re: [Coq-Club] Coq 8.6 and Ocaml 4.06, Théo Zimmermann, 11/23/2017
        
        Re: [Coq-Club] Coq 8.6 and Ocaml 4.06, Pierre Courtieu, 11/23/2017