问comparable.vo包含库Top.comparable，但不包含库可比库
EN

Stack Overflow用户

提问于 2020-05-02 22:31:43

回答 1查看 115关注 0票数 1

我是Coq的新手。

在我们的项目中，我们切换到使用coq_makefile实用程序，并遇到了以下问题。

单步执行验证脚本将导致以下错误：

Require Import comparable.

Error:
The file /Users/ayman/open-source/regex-reexamined-coq/comparable.vo contains library
Top.comparable and not library comparable

我们的_CoqProject文件非常简单(也许这就是问题所在)，它只列出了项目https://github.com/awalterschulze/regex-reexamined-coq/blob/2c865aecc00276e0a926c1729cc35553c1cc6767/_CoqProject中的所有文件。

coq

回答 1

Stack Overflow用户

回答已采纳

发布于 2020-05-08 22:36:20

Coq库有一个逻辑路径。例如，标准库中的所有文件都有一个以Coq开头的逻辑路径。在本例中，您没有指定任何有关逻辑路径的内容，因此Coq会将编译后的文件放入以Top开头的路径中。稍后，当尝试加载文件时，Coq会将逻辑路径Top与物理路径.进行比较，并抱怨差异。

最简单的解决方法是将以下行添加到_CoqProject文件中：-R . Top。选项-R将物理路径(这里是.)映射到逻辑路径(这里是Top)，这将修复差异。

但是对于一个库来说，Top不是一个好名字，所以你应该用其他东西来代替它。此外，该名称将作为库的安装路径，因此请选择一个有意义的名称(例如，RegexDerivatives)，因为这是用户将使用的名称。

票数 2

页面原文内容由Stack Overflow提供。腾讯云小微IT领域专用引擎提供翻译支持

原文链接：

https://stackoverflow.com/questions/61561014

复制

相似问题

问comparable.vo包含库Top.comparable，但不包含库可比库
EN

回答 1

Stack Overflow用户

社区

活动

圈层

关于

腾讯云开发者

热门产品

热门推荐

更多推荐

问comparable.vo包含库Top.comparable，但不包含库可比库EN

回答 1

Stack Overflow用户

社区

活动

圈层

关于

腾讯云开发者

热门产品

热门推荐

更多推荐

问comparable.vo包含库Top.comparable，但不包含库可比库
EN