Coq 在 Omega 上失败

Question

我正在尝试遵循 this 但提供的源文件失败 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. 上似乎成功了。

Answer 1

Omega 模块和 omega 策略已在 Coq 8.14 版中删除（在 8.12 版中弃用后）。

最新的CPDT tarball似乎还没有更新，无法兼容Coq 8.14，所以这意味着你应该用较低版本的Coq编译它，比如8.13版本。

您可以通过 Coq Platform.

安装较早版本的 Coq

如果您使用 Coq 平台脚本，您可以依赖最新版本的 Coq 平台，因为它提供了 select 早期版本 Coq 的选项。如果您更愿意使用二进制安装程序，那么您可以在 previous release of the Platform.

中找到 Coq 8.13 的安装程序

之所以 Require Import Omega 在 https://x80.org/collacoq is that this website has not been kept up-to-date and is still at Coq version 8.11. If you use https://coq.vercel.app/scratchpad.html 上运行，是因为您获得了最新版本的 Coq（因此 Require Import Omega 不起作用）。

Coq 在 Omega 上失败

Coq make failing on Omega

coq