Coq make failing on Omega

Question

我试图遵循这一点，但提供的源文件失败的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.

我已经在我的custom-set-variables

'(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平台来安装Coq的早期版本。

如果您使用Coq平台脚本，您可以依赖于Coq平台的最新版本，因为它提供了选择Coq早期版本的选项。如果您更愿意使用二进制安装程序，那么您可以在平台的先前版本中找到Coq 8.13的安装程序。

Require Import Omega在https://x80.org/collacoq上工作的原因是这个网站没有保持最新，仍然是Coq 8.11版本。如果您使用https://coq.vercel.app/scratchpad.html，您将获得最新版本的Coq(因此Require Import Omega无法工作)。