How do I install a library in coq? (MacOS)

Question

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.

Answer 1

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.

Answer 2

When you write Require Import X., this tells Coq to look for X in either the place specified by your _CoqProject or in the Coq standard library (although the latter one might not be true in the future). When you want to use libraries from some other place Y, you should tell Coq like this:

From Y Require Import X.

In your case, there is no need to add anything about mathcomp to your _CoqProject, because it has already been installed in a place Coq will look for if you let it know it should look for it with From mathcomp .... The typical incantation when you want to use the basic mathcomp librarly, called ssreflect, is to write:

From mathcomp Require Import all_ssreflect.

In order to use finmap:

From mathcomp Require Import finmap.

Some natural questions given your remarks above:

Q: Why did Require Import ssreflect. work?

A: There is a library called ssreflect in the Coq standard library, that's the one this command imports.

Q: Why didn't From mathcomp Require Import all_ssreflect all_fingroup. work?

A: You didn't install coq-mathcomp-fingroup, probably because you don't need it. Plausibly Pierre got it confused with finmap.

Q: Wait, ssreflect is both a mathcomp library and a Coq library?

A: I was confused by this for a while. Basically ssreflect is the name of a tactic language that was originally developed for mathcomp but has since been integrated into Coq itself. However, ssreflect happens to still be the name of the most basic mathcomp package too. Thus, Require Import ssreflect. gets you only the tactic language, but From mathcomp Require Import all_ssreflect. gets you both the tactic language and a new standard library with definitions and results about natural numbers, lists, ordinals, and so on. Other more specialized mathcomp libraries need to be installed separately, such as finmap or fingroup.

Answer 3

For me, one magic mantra on my Mac using Coq via nix is:

From mathcomp Require Import all_ssreflect all_fingroup.