Модуль Coq Не удается найти физический путь, связанный с суффиксом соответствия логического пути ‹› и префиксом и не найденный в пути загрузки

Я читаю логические основы и скачал поставляемые скрипты coq с этим.

Пользуюсь coq v8.8.1, установка через opam.

Я получаю две ошибки в заголовке, и я не уверен, как мне их отлаживать.

Полное сообщение об ошибке для второй ошибки:

COQDEP VFILES

*** Предупреждение: в файле Auto.v требуется библиотека LF.Maps, и она не найдена в пути загрузки!

Моя цель - скомпилировать и запустить файл Induction.v. Я использовал параметры coqide, чтобы сначала создать файл makefile, а затем сделать его, прежде чем я получил эти ошибки.


coq coqide
person Peeyush Kushwaha    schedule 04.04.2019    source источник
comment
Software Foundation поставляется с собственным make-файлом. Попробуйте распаковать архив и запустить make в каталоге верхнего уровня без использования make-файла coqide.   -  person Arthur Azevedo De Amorim    schedule 04.04.2019
comment
Вы также можете проверить, были ли созданы файлы * .vo. Это скомпилированные файлы * .v, поэтому их наличие указывает на то, были ли исходные файлы скомпилированы успешно.   -  person eponier    schedule 05.04.2019

Ответы (1)


arrow_upward
0
arrow_downward

Это сработало для меня:

Запустите это в том же каталоге, что и Basics.v

coqc -Q . LF Basics.v

А потом...

  • Мне удалось скомпилировать Induction.v:

    coqc -Q . LF Induction.v

  • И мне удалось это сделать:

    coqtop -Q . LF
{* now that coqtop is open... *}
From LF Require Export Basics.
person pianoJames    schedule 25.01.2021