Skip to Content.
Sympa Menu

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

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Coq 8.6 and Ocaml 4.06


Chronological Thread 
  • 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



Archive powered by MHonArc 2.6.18.

Top of Page