coq - Coq 使 Omega 失败

我正在尝试关注 http://adam.chlipala.net/cpdt/ 但提供的源文件失败 make 并出现此错误

make[1]: Entering directory '/home/myhome/Dropbox/org/coq/cpdt'
COQC src/CpdtTactics.v
File "./src/CpdtTactics.v", line 10, characters 0-32:
Error: Cannot find a physical path bound to logical path Omega.

CpdtTactics.v 中有

...
Require Import Eqdep List Omega.
...

这个 Omega 在哪里?一个参考提到它已被弃用。另一个人可能提到了 ZArith 作为替代品。此外,只需调用 cpdt/src 文件的 InductiveTypes.v 并尝试逐行评估,我得到

Error: Cannot find a physical path bound to logical path Cpdt.CpdtTactics.

我的自定义设置变量中有这个

'(coq-prog-args
   '("-emacs -R /home/myhome/Dropbox/org/coq/cpdt/src Cpdt"))

但我猜这不一定是我的错误,而是 coq 正在寻找 CpdtTactics.vo 而它不存在,因为 make 没有完成? (事实上,它不存在。)

我在 coq 8.15 并且正在使用 Emacs 28.1/Proof General Version 4.5-git。

顺便说一句,在 https://x80.org/collacoq/ Require Import Omega. 上似乎成功了。

回答1

Omega 模块和 omega 策略已在 Coq 版本 8.14 中删除(在版本 8.12 中被弃用之后)。

似乎最新的 CPDT tarball 尚未更新为与 Coq 8.14 兼容,因此这意味着您应该使用较低版本的 Coq 编译它,例如版本 8.13。

您可以依靠 https://github.com/coq/platform/releases 安装早期版本的 Coq。

如果您使用 Coq 平台脚本,您可以依赖最新版本的 Coq 平台,因为它提供了选择早期版本 Coq 的选项。如果您更愿意使用二进制安装程序,那么您可以在 https://github.com/coq/platform/releases/tag/2021.09.0中找到 Coq 8.13 的安装程序。

Require Import Omega 之所以能在 https://x80.org/collacoq 上工作,是因为这个网站没有跟上-date,仍然是Coq 8.11 版本。如果您改用 https://coq.vercel.app/scratchpad.html,您将获得最新版本的 Coq(因此 Require Import Omega 不起作用)。

相似文章

coq - Coq - 将表达式赋值给变量

首先,我还不太熟悉Coq行话,所以我会使用诸如“表达式”和“变量”比较松散,但它们可能不是正确的Coq术语。我正在尝试证明定理的以下子目标。1goalb:bagv,b':natb'':natlistB...

最新文章