Я новичок в Coq и в настоящее время просматриваю серию руководств по основам программного обеспечения.
Тем не менее, я продолжаю бороться с тем, чтобы часть Require Export
работала с первой попытки, и каждый файл, по-видимому, требовал новой стратегии для работы. На этот раз, однако, я застрял полностью.
В одном файле (Lists.v) я могу просто написать
From LF Require Export Induction.
, и пусть работает нормально.
В следующем же (Poly.v) вообще не могу загрузить модуль Lists,
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.
@eponier это вывод пути загрузки печати: pastebin.com/ZAQa8QL0 И я компилирую каждый файл по отдельности, прежде чем импортировать его одинаково по всем направлениям.
Спасибо за подробности. Но я имел в виду следующее: вы используете make
или кнопку меню CoqIDE для компиляции?
В любом случае, вам не нужно использовать Add LoadPath
. _CoqProject
должно быть достаточно.
Я использую кнопку меню, make не работает. И я знаю, что не должен использовать Add Loadpath, но, как я уже сказал, он не работает ни в одном из файлов без него.
Можете ли вы построить через командную строку вместо этого? cd ~/.../LF
и coqc -Q . LF Poly.v
. Поскольку coqide, похоже, не распознает _CoqProject
, но вы все равно можете указать ему, где найти файлы, то возможность создавать файлы с правильными параметрами должна позволить вам двигаться вперед. Кроме того, Add LoadPath "~/.../LF" as LF.
будет эквивалентом -Q . LF
, чтобы избежать несоответствия между тем, как вещи компилируются, и тем, как их ищет coqide.
Он отлично компилируется в консоли без явного пути загрузки, но IDE отказывается анализировать строку Require Export
.
Закрытие среды IDE и ее повторное открытие, похоже, волшебным образом решили проблему.
Когда вы создаете новый файл, CoqIDE не может использовать его местоположение для поиска связанного _CoqProject
, пока он не будет сохранен. И даже при сохранении не учитывает сразу. Вы должны закрыть вкладку и снова открыть файл, чтобы все заработало.
Когда вы используете кнопку меню, она показывает команду, которая фактически используется для компиляции, так что вы можете проверить, правильно ли передана опция coqc
. В частности, -Q . LF
.
Судя по всему, вы не компилируете и не загружаете файлы последовательно, то есть с учетом
-Q . LF
_CoqProject
. Не могли бы вы объяснить, как вы компилируете файлы? А не могли бы вы показать, что выдаетPrint LoadPath
?