Coq在Omega上失败
我正在尝试跟踪这，但是提供的源文件出现了错误，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/验证通用版本4.5-git。
顺便说一句，https://x80.org/collacoq/ Require Import Omega.似乎成功了。
回答 1
Stack Overflow用户
发布于 2022-05-18 23:01:33
Omega模块和omega策略已经在COQ8.14版本中被删除(在8.12版本中被废弃后)。
最近的CPDT tarball似乎还没有更新以与Coq 8.14兼容，因此这意味着您应该使用较低版本的Coq编译它，比如版本8.13。
您可以通过依赖Coq平台安装Coq的早期版本。
如果使用Coq平台脚本，则可以依赖Coq平台的最新版本，因为它提供了选择Coq早期版本的选项。如果您更愿意使用二进制安装程序，那么可以在平台的前一个版本中找到Coq8.13的安装程序。
Require Import Omega之所以在https://x80.org/collacoq上工作，是因为这个网站还没有被更新，而且仍然处于Coq版本8.11。如果您使用https://coq.vercel.app/scratchpad.html，您将得到Coq的最新版本(因此Require Import Omega无法工作)。
https://stackoverflow.com/questions/72298228
复制
腾讯云开发者
