时间戳

首页 > 解决方案 > coq 8.11.0 与 ocaml 4.10 不兼容？

ocaml - coq 8.11.0 与 ocaml 4.10 不兼容？

问题描述

我正在按照这些说明使用 opam 安装 coq并收到错误消息

`No solution for coq: The following dependencies couldn't be met:
          - coq → ocaml < 4.10
              base of this switch (use '--unlock-base' to force)

我继续使用以下命令切换到 ocaml 4.05.0

opam switch create with-coq 4.05.0

并且可以成功安装 Coq，但我更愿意使用 ocaml 的更新版本。这是 Coq 和 oCaml 之间的实际不兼容，还是我做错了什么？

为了增加上下文，我现在使用 opam 2.0.6、ocaml 版本 4.05.0 和 Coq 版本 8.11.0。我的操作系统是 macOS。之前，唯一的区别是我尝试使用 ocaml 4.10.0。

谢谢！

标签： ocamlcoqopam

解决方案

您需要 v8.11 分支的提示或等待应该很快发布的 8.11.1。

你不需要回到 4.05.0，4.09 可以正常工作，但 4.07.1+flambda 是我推荐的，请参阅https://coq.discourse.group/t/install-notes-on- coq-and-ocaml-versions-configuration/713

推荐阅读