Конфигурация CoqIDE в Linux

Question

У меня свежая установка Coq 8.6 в Ubuntu 17.04. Когда я пытаюсь скомпилировать свой проект, используя make, он работает нормально, пока не получит первое сообщение об ошибке. Затем я пытаюсь использовать CoqIDE, чтобы найти и исправить ошибку, но я получаю новые сообщения об ошибках, такие как:

"Файл foo.vo содержит библиотеку Top.foo, а не библиотеку foo"

Я думаю, что что-то не так с конфигурацией CoqIDE, но я не знаю, что это может быть. Есть намеки?

Заранее спасибо, Маркус.

Answer 1

Я думаю, что вы сейчас стоите в каталоге с файлом foo.vo

Для сопоставления файлов в текущем каталоге . в пространство имен Top вы приводите аргумент

-Q . Top

Вот "полный" пример.

mkdir test; cd test
echo 'Definition a:=1.' > foo.v

coqc -Q . Top foo.v    # this puts the foo module into Top as Top.foo.

coqtop -Q . Top

Coq <  Require Import Top.foo. Print a.

a = 1
     : nat

но использование coqtop без сопоставления.vo с пространством имен, в которое он был скомпилирован, завершается неудачно:

coqtop

Coq <  Require foo.

> Require foo.
> ^^^^^^^^^^^^
Error: The file /.../test/foo.vo contains library Top.foo
and not library foo