Требовать экспорт изменений требований в каждом файле
Я новичок в 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.