我正在尝试关注 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文件的 encuctivetypes.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版本4.5-GIT。
顺便说一句， https://x80.org/collacoq/ 要求导入Omega。似乎成功了。
I'm trying to follow this but the provided source files are failing make with this error
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.
in CpdtTactics.v there is
...
Require Import Eqdep List Omega.
...
Where is this Omega? One reference mentioned it being deprecated. Another might have mentioned ZArith as a substitute. Also, just calling up InductiveTypes.v of the cpdt/src files and trying to evaluate line-by-line, I get
Error: Cannot find a physical path bound to logical path Cpdt.CpdtTactics.
I've got this in my custom-set-variables
'(coq-prog-args
'("-emacs -R /home/myhome/Dropbox/org/coq/cpdt/src Cpdt"))
But I'm guessing this is not necessarily my mistake, rather, coq is looking for CpdtTactics.vo and it's not there because make didn't complete? (In fact, it's not there.)
I'm on coq 8.15 and am using Emacs 28.1/Proof General Version 4.5-git.
BTW, on https://x80.org/collacoq/ Require Import Omega. seems to succeed.
发布评论
评论（1）
Omega模块和Omega策略已在COQ版本8.14中删除（在版本8.12中被弃用后）。看来最新的CPDT TARBALL尚未更新与COQ 8.14兼容，因此这意味着您应该使用较低版本的COQ（例如8.13版）对其进行编译。
您可以通过依靠 coq平台来安装COQ的早期版本。
如果使用COQ平台脚本，则可以依靠COQ平台的最新版本，因为它提供了选择早期版本COQ的选项。如果您想使用二进制安装程序，则可以在a 平台的先前版本。
需要导入omega在 https://coq.vercel.app/scratchpad.html 相反，您得到了COQ的最新版本（因此需要导入Omega不起作用）。The
Omegamodule and theomegatactic have been removed in Coq version 8.14 (after being deprecated in version 8.12).It seems that the latest CPDT tarball was not updated yet to be compatible with Coq 8.14, so this means that you should compile it with a lower version of Coq, such as version 8.13.
You can install earlier versions of Coq by relying on the Coq Platform.
If you use the Coq Platform scripts, you can rely on the latest version of the Coq Platform since it provides the option to select an earlier version of Coq. If you'd rather use the binary installers, then you can find installers for Coq 8.13 in a previous release of the Platform.
The reason why
Require Import Omegaworks on 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 instead, you get the latest version of Coq (and thusRequire Import Omegadoes not work).