2
$\begingroup$

There's this library I'd like to use. The idea is to be able to use this library with Require Import easily in any other *.v file.

In the readme of said library, it recommends to include the library in my developments. So I understand I should add to the _CoqProject of this library (and not of any other new project which will use this library) the path to the directory that contains the _CoqProject file of this library.

Then I

coq_makefile -f _CoqProject -o Makefile
make
make install

as is recommended in this stackoverflow answer.

However, when I make, I get the following error.

I just downloaded the library and put it in some random directory to do this. Should it be somewhere in particular instead?

Sadly the coq.inria webpage seems to be down for the time being so I can't check the official documentation on _CoqProject for which I know almost nothing about.

Thanks in advance for any help!

Improve this question
$\endgroup$

1 Answer 1

Reset to default
5
$\begingroup$

If you use opam, it should just be as simple as

git clone https://github.com/jwiegley/category-theory
cd category-theory
opam install .

Once complete, add Require Import Category.Theory. into any Coq file.

Improve this answer
$\endgroup$
2
  • $\begingroup$ Hey, thanks for the answer! When I try to opam install ., it says I'm missing coq-equations as a dependency, and if I try to install coq-equations the same way, it says it's missing coq >= dev. If I go to the coq-equations webpage and do what they suggest, the installation breakes since it appears it depends on coq.inria.fr which has been down for some time, but reading what they suggest doing, I'm not so sure that dependency problem would've been overcome. Do you have any suggestions on how to do this properly? (given that opam install . works otherwise.) $\endgroup$
    – Julián
    Commented Aug 13, 2023 at 23:34
  • 2
    $\begingroup$ It seems you've already asked this question on the Coq Zulip and gotten a solution, but for the benefit of self-hosting the answer, it's: git clone https://github.com/coq/opam-coq-archive; cd opam-coq-archive/; opam repo add --kind local coq-fork ./released/ $\endgroup$
    – djao
    Commented Aug 15, 2023 at 16:43

Not the answer you're looking for? Browse other questions tagged or ask your own question.