comparable.vo包含库Top.comparable，但与库不具有可比性

Question

我对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中的所有文件。

Answer 1

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

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

但是Top对于库来说是个坏名字，因此您应该用其他名称替换它。此外，该名称将用作您库的安装路径，因此请选择一个有意义的名称（例如RegexDerivatives），因为该名称是用户将使用的名称。