coq - 在同一个库中导出模块时出现 CoqIDE 错误

Question

我正在运行 CoqIDE 来阅读教科书系列“软件基础”，我目前正在阅读“逻辑基础”一卷。我刚开始第 2 章（归纳），但是当我尝试运行时

From LF Require Import Basics.

我收到错误声明

The file ...\LF\Basics.vo contains library Basics and not library LF.Basics

我尝试重命名文件所在的目录，并重新编译缓冲区，但这些操作都没有帮助。我应该怎么做才能解决这个问题？

Answer 1

我们一直在改进即将发布的新版 LF 中的解释。这是相关的位：

For the [Require Export] to work, Coq needs to be able to
find a compiled version of [Basics.v], called [Basics.vo], in a directory
associated with the prefix [LF].  This file is analogous to the [.class]
files compiled from [.java] source files and the [.o] files compiled from
[.c] files.

First create a file named [_CoqProject] containing the following line
(if you obtained the whole volume "Logical Foundations" as a single
archive, a [_CoqProject] should already exist and you can skip this step):

  [-Q . LF]

This maps the current directory ("[.]", which contains [Basics.v],
[Induction.v], etc.) to the prefix (or "logical directory") "[LF]".
PG and CoqIDE read [_CoqProject] automatically, so they know to where to
look for the file [Basics.vo] corresponding to the library [LF.Basics].

Once [_CoqProject] is thus created, there are various ways to build
[Basics.vo]:

 - In Proof General: The compilation can be made to happen automatically
   when you submit the [Require] line above to PG, by setting the emacs
   variable [coq-compile-before-require] to [t].

 - In CoqIDE: Open [Basics.v]; then, in the "Compile" menu, click
   on "Compile Buffer".

 - From the command line: Generate a [Makefile] using the [coq_makefile]
   utility, that comes installed with Coq (if you obtained the whole
   volume as a single archive, a [Makefile] should already exist
   and you can skip this step):

     [coq_makefile -f _CoqProject *.v -o Makefile]

   Note: You should rerun that command whenever you add or remove Coq files
   to the directory.

   Then you can compile [Basics.v] by running [make] with the corresponding
   [.vo] file as a target:

     [make Basics.vo]

   All files in the directory can be compiled by giving no arguments:

     [make]

   Under the hood, [make] uses the Coq compiler, [coqc].  You can also
   run [coqc] directly:

     [coqc -Q . LF Basics.v]

   But [make] also calculates dependencies between source files to compile
   them in the right order, so [make] should generally be prefered over
   explicit [coqc].

If you have trouble (e.g., if you get complaints about missing
identifiers later in the file), it may be because the "load path"
for Coq is not set up correctly.  The [Print LoadPath.] command
may be helpful in sorting out such issues.

In particular, if you see a message like

    [Compiled library Foo makes inconsistent assumptions over
    library Bar]

check whether you have multiple installations of Coq on your machine.
It may be that commands (like [coqc]) that you execute in a terminal
window are getting a different version of Coq than commands executed by
Proof General or CoqIDE.

- Another common reason is that the library [Bar] was modified and
  recompiled without also recompiling [Foo] which depends on it.  Recompile
  [Foo], or everything if too many files are affected.  (Using the third
  solution above: [make clean; make].)

One more tip for CoqIDE users: If you see messages like [Error:
Unable to locate library Basics], a likely reason is
inconsistencies between compiling things _within CoqIDE_ vs _using
[coqc] from the command line_.  This typically happens when there
are two incompatible versions of [coqc] installed on your
system (one associated with CoqIDE, and one associated with [coqc]
from the terminal).  The workaround for this situation is
compiling using CoqIDE only (i.e. choosing "make" from the menu),
and avoiding using [coqc] directly at all. *)