Требовать экспорт изменений требований в каждом файле - PullRequest
Новая
       79

Требовать экспорт изменений требований в каждом файле

0 голосов
/ 07 февраля 2019

Я новичок в Coq, и в настоящее время изучаю серию учебных пособий Software Foundations.

Тем не менее, я продолжаю бороться с тем, чтобы часть Require Export работала с первой попытки, каждый файл на первый взглядтребует новой стратегии для работы.На этот раз, однако, я застрял полностью.

В одном файле (Lists.v) я могу просто написать From LF Require Export Induction., и у меня это работает просто отлично.

В самомследующий (Poly.v), я вообще не могу загрузить модуль списков, 

From LF Require Export Lists. 
(* ==> Cannot find a physical path bound to logical path matching suffix
<> and prefix LF. *)

Если я сначала не добавлю путь загрузки в текущую папку: 

Add LoadPath "~/Documents/code/coq/".
From LF Require Export Lists. (* Works perfectly! *)

Однако, в следующей главе, и, кажется, ничего не работает.

Вот что я попробовал: 

From LF Require Export Poly.
(* ==> Cannot find a physical path bound to logical path matching suffix
<> and prefix LF. *)

Add LoadPath "~/Documents/code/coq/".
From LF Require Export Poly.
(* ==> The file /Users/coffee/Documents/code/coq/LF/Poly.vo contains library Poly
and not library LF.Poly *)

Add LoadPath "~/Documents/code/coq/LF/".
From LF Require Export Poly.
(* ==> Cannot find a physical path bound to logical path matching suffix
<> and prefix LF. *)

Add LoadPath "~/Documents/code/coq/LF/".
Require Export Poly.
(* ==> Cannot load LF.Basics: no physical path bound to LF *)

Можно с уверенностью сказать: я в растерянности, я понятия не имею, что я делаю или почему это не работает.Он работал раньше, и ничего, что я могу найти в Интернете, похоже, не дает хороших ответов.

Мой файл _CoqProject содержит -Q . LF

Я испытываю эту проблему как на Windows, так и на Mac.

И я использую последнюю версию CoqIDE.

...