Coqtop не может загрузить файл - PullRequest
Новая
       3

Coqtop не может загрузить файл

0 голосов
/ 04 марта 2020

Я сейчас работаю над Software Foundations - Logical Foundation.

Короче, я получил ошибку Error: Cannot find a physical path bound to logical path matching suffix <> and prefix LF.

У меня установлен Coq brew.

У меня есть следующие файлы, расположенные в ~/Documents/Notes/PL/SF/LF/

  • _CoqProject содержит одну строку: -Q . LF
  • Basics.v содержит код для первой главы
  • Makefile генерируется командой coq_makefile -f _CoqProject *.v -o Makefile

Затем я делаю Basics.vo с помощью make Basics.vo

Теперь я открываю coqtop и пытаюсь запустить команда From LF Require Export Basics. и вот как это выглядит 

╭─~/Documents/Notes/PL/SF/LF
╰─$ coqtop

Welcome to Coq 8.11.0 (January 2020)

Coq < From LF Require Export Basics.

Toplevel input, characters 23-29:
> From LF Require Export Basics.
>                        ^^^^^^
Error: Cannot find a physical path bound to logical path matching suffix
<> and prefix LF

Вот вывод Print LoadPath.. Последняя строка вывода ясно показывает <> /Users/myname/Documents/Notes/PL/SF/LF, для чего я не знаю, что это значит. 

Coq <
Coq < Print LoadPath.
Logical Path / Physical path:
<> /usr/local/Cellar/coq/8.11.0/share/coq
latex /usr/local/Cellar/coq/8.11.0/share/coq/latex
<> /usr/local/Cellar/coq/8.11.0/lib/coq/user-contrib
Ltac2 /usr/local/Cellar/coq/8.11.0/lib/coq/user-contrib/Ltac2
Coq /usr/local/Cellar/coq/8.11.0/lib/coq/plugins
Coq.firstorder /usr/local/Cellar/coq/8.11.0/lib/coq/plugins/firstorder
Coq.ltac /usr/local/Cellar/coq/8.11.0/lib/coq/plugins/ltac
Coq.extraction /usr/local/Cellar/coq/8.11.0/lib/coq/plugins/extraction
Coq.btauto /usr/local/Cellar/coq/8.11.0/lib/coq/plugins/btauto
Coq.syntax /usr/local/Cellar/coq/8.11.0/lib/coq/plugins/syntax
Coq.nsatz /usr/local/Cellar/coq/8.11.0/lib/coq/plugins/nsatz
Coq.omega /usr/local/Cellar/coq/8.11.0/lib/coq/plugins/omega
Coq.cc /usr/local/Cellar/coq/8.11.0/lib/coq/plugins/cc
Coq.derive /usr/local/Cellar/coq/8.11.0/lib/coq/plugins/derive
Coq.ssr /usr/local/Cellar/coq/8.11.0/lib/coq/plugins/ssr
Coq.rtauto /usr/local/Cellar/coq/8.11.0/lib/coq/plugins/rtauto
Coq.micromega /usr/local/Cellar/coq/8.11.0/lib/coq/plugins/micromega
Coq.funind /usr/local/Cellar/coq/8.11.0/lib/coq/plugins/funind
Coq.setoid_ring /usr/local/Cellar/coq/8.11.0/lib/coq/plugins/setoid_ring
Coq.ssrmatching /usr/local/Cellar/coq/8.11.0/lib/coq/plugins/ssrmatching
Coq /usr/local/Cellar/coq/8.11.0/lib/coq/theories
Coq.PArith /usr/local/Cellar/coq/8.11.0/lib/coq/theories/PArith
Coq.MSets /usr/local/Cellar/coq/8.11.0/lib/coq/theories/MSets
Coq.QArith /usr/local/Cellar/coq/8.11.0/lib/coq/theories/QArith
Coq.Sorting /usr/local/Cellar/coq/8.11.0/lib/coq/theories/Sorting
Coq.Program /usr/local/Cellar/coq/8.11.0/lib/coq/theories/Program
Coq.ZArith /usr/local/Cellar/coq/8.11.0/lib/coq/theories/ZArith
Coq.Bool /usr/local/Cellar/coq/8.11.0/lib/coq/theories/Bool
Coq.Sets /usr/local/Cellar/coq/8.11.0/lib/coq/theories/Sets
Coq.NArith /usr/local/Cellar/coq/8.11.0/lib/coq/theories/NArith
Coq.Wellfounded /usr/local/Cellar/coq/8.11.0/lib/coq/theories/Wellfounded
Coq.Arith /usr/local/Cellar/coq/8.11.0/lib/coq/theories/Arith
Coq.Vectors /usr/local/Cellar/coq/8.11.0/lib/coq/theories/Vectors
Coq.Reals /usr/local/Cellar/coq/8.11.0/lib/coq/theories/Reals
Coq.Logic /usr/local/Cellar/coq/8.11.0/lib/coq/theories/Logic
Coq.Floats /usr/local/Cellar/coq/8.11.0/lib/coq/theories/Floats
Coq.Classes /usr/local/Cellar/coq/8.11.0/lib/coq/theories/Classes
Coq.Lists /usr/local/Cellar/coq/8.11.0/lib/coq/theories/Lists
Coq.Relations /usr/local/Cellar/coq/8.11.0/lib/coq/theories/Relations
Coq.Unicode /usr/local/Cellar/coq/8.11.0/lib/coq/theories/Unicode
Coq.Structures /usr/local/Cellar/coq/8.11.0/lib/coq/theories/Structures
Coq.Setoids /usr/local/Cellar/coq/8.11.0/lib/coq/theories/Setoids
Coq.Numbers.Integer.Binary
  /usr/local/Cellar/coq/8.11.0/lib/coq/theories/Numbers/Integer/Binary
Coq.Numbers.Integer.NatPairs
  /usr/local/Cellar/coq/8.11.0/lib/coq/theories/Numbers/Integer/NatPairs
Coq.Numbers.Integer.Abstract
  /usr/local/Cellar/coq/8.11.0/lib/coq/theories/Numbers/Integer/Abstract
Coq.Numbers.Integer
  /usr/local/Cellar/coq/8.11.0/lib/coq/theories/Numbers/Integer
Coq.Numbers.NatInt
  /usr/local/Cellar/coq/8.11.0/lib/coq/theories/Numbers/NatInt
Coq.Numbers.Natural.Binary
  /usr/local/Cellar/coq/8.11.0/lib/coq/theories/Numbers/Natural/Binary
Coq.Numbers.Natural.Peano
  /usr/local/Cellar/coq/8.11.0/lib/coq/theories/Numbers/Natural/Peano
Coq.Numbers.Natural.Abstract
  /usr/local/Cellar/coq/8.11.0/lib/coq/theories/Numbers/Natural/Abstract
Coq.Numbers.Natural
  /usr/local/Cellar/coq/8.11.0/lib/coq/theories/Numbers/Natural
Coq.Numbers.Cyclic.Int63
  /usr/local/Cellar/coq/8.11.0/lib/coq/theories/Numbers/Cyclic/Int63
Coq.Numbers.Cyclic.Int31
  /usr/local/Cellar/coq/8.11.0/lib/coq/theories/Numbers/Cyclic/Int31
Coq.Numbers.Cyclic.ZModulo
  /usr/local/Cellar/coq/8.11.0/lib/coq/theories/Numbers/Cyclic/ZModulo
Coq.Numbers.Cyclic.Abstract
  /usr/local/Cellar/coq/8.11.0/lib/coq/theories/Numbers/Cyclic/Abstract
Coq.Numbers.Cyclic
  /usr/local/Cellar/coq/8.11.0/lib/coq/theories/Numbers/Cyclic
Coq.Numbers /usr/local/Cellar/coq/8.11.0/lib/coq/theories/Numbers
Coq.Compat /usr/local/Cellar/coq/8.11.0/lib/coq/theories/Compat
Coq.Strings /usr/local/Cellar/coq/8.11.0/lib/coq/theories/Strings
Coq.Init /usr/local/Cellar/coq/8.11.0/lib/coq/theories/Init
Coq.FSets /usr/local/Cellar/coq/8.11.0/lib/coq/theories/FSets
<> /Users/myname/Documents/Notes/PL/SF/LF

Может кто-нибудь помочь мне выяснить, что произошло?

1 Ответ

0 голосов
/ 04 марта 2020

Вам необходимо связать текущий каталог (.../LF) с префиксом LF: 

(* In coqtop *)
Add LoadPath "." as LF.

(* So that... *)
Print LoadPath.
(* shows:
     ...
     LF /Users/.../LF
*)

Я также слышал, что прямое использование coqtop настоятельно не рекомендуется, и вместо этого рекомендуется использовать правильный редактор (VSCode, Emacs + Proof General, CoqIDE).

...