Coqtop cannot load file

I'm currently working on Software Foundations – Logical Foundation.

In short, I got error Error: Cannot find a physical path bound to logical path matching suffix <> and prefix LF.

I have Coq brew installed.

I have the following files located at ~/Documents/Notes/PL/SF/LF/

_CoqProject contains single line: -Q . LF
Basics.v contains code for the first chapter
Makefile generated by command coq_makefile -f _CoqProject *.v -o Makefile

Then I make Basics.vo by make Basics.vo

Now I open coqtop, and try to run the command From LF Require Export Basics. and here is what it looks like

╭─~/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

Here is the output of Print LoadPath.. The last line of the output clearly shows <> /Users/myname/Documents/Notes/PL/SF/LF, for which I don't know what does it mean.

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

Can anyone help me figure out what happened?

Solution

You need to associate the current directory (.../LF) to the LF prefix:

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

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

I also heard that directly using coqtop is strongly discouraged, and instead it is recommended to use a proper editor (VSCode, Emacs + Proof General, CoqIDE).