I'm trying to work with the mathcomp library in VSCoq. I followed the installation instructions on the library website.
opam repo add coq-released https://coq.inria.fr/opam/released
opam install coq-mathcomp-ssreflect
opam install coq-mathcomp-finmap
This didn't change my local directory structure, so I added the relevant information to my _CoqProject file.
_CoqProject:
-Q /Users/<user>/.opam/default/lib/coq/user-contrib/mathcomp Mathcomp
.
I tested that this works fine with relative paths to other libraries I have installed.
In my .v file, I can't import finmap despite installing it, but I can import ssreflect.
Require Import ssreflect.
Require Import finmap.
gives me the error
Error: Cannot find a physical path bound to logical path finmap.
I have no idea why ssreflect is imported with no problem but finmap is not.
Thank you for the responses. Although they did not fix the problem, they were extremely helpful in understanding how Coq dependencies work, especially because of the lack of detailed documentation.
After all the packages were installed using opam, the issue persisted. It turns out, when using vscoq, it is one must reload the window before installed dependencies are recognized.
So, reloading VSCode did the trick.