我正在尝试关注 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 不起作用）。