Stream: Coq users

Topic: ✔ HoTT library installation

view this post on Zulip Callan McGill (Jan 25 2022 at 16:37):

I am trying to use the HoTT library but I get the message: Unable to locate library HoTT. (While searching for a .vos file). I have a _CoqProject file containing:

-arg -noinit
-arg -indices-matter

I have installed coq via opam and then installed the coq-prover via snap so I may need to configure something, does anyone have any ideas of the easiest path forward?

view this post on Zulip Ali Caglayan (Jan 25 2022 at 16:56):

Do you get the message in coqide?

view this post on Zulip Ali Caglayan (Jan 25 2022 at 16:57):

Did you start coqide in the same directory as your _CoqProject?

view this post on Zulip Karl Palmskog (Jan 25 2022 at 16:59):

from what I remember, installing both Coq via opam and then installing the Snap will typically lead to issues. It sounds like the project is only picking up the opam installation, which doesn't have HoTT.

view this post on Zulip Ali Caglayan (Jan 25 2022 at 17:02):

Oh yes that's probably it. HoTT does have an opam release, and I would encourage you to use that rather than whatever is in the snap package. You may need to add the opam repos for coq libraries however

view this post on Zulip Ali Caglayan (Jan 25 2022 at 17:02):

opam repo add coq-released https://coq.inria.fr/opam/released

view this post on Zulip Ali Caglayan (Jan 25 2022 at 17:02):

for released versions of HoTT (there should be one for each released version of coq)

view this post on Zulip Ali Caglayan (Jan 25 2022 at 17:02):

opam repo add coq-extra-dev https://coq.inria.fr/opam/extra-dev if you are using coq master

view this post on Zulip Ali Caglayan (Jan 25 2022 at 17:03):

after that opam install coq-hott should install HoTT properly

view this post on Zulip Karl Palmskog (Jan 25 2022 at 17:04):

(avoid the extra-dev opam repo if possible, and in general Coq master can be hard to use)

view this post on Zulip Michael Soegtrop (Jan 25 2022 at 17:33):

You might want to use (https://github.com/coq/platform). It sets up opam in the proper way. You can just install base coq (various versions) and then add HoTT via opam - or install the full Coq Platform right away which includes HoTT.

view this post on Zulip Callan McGill (Jan 25 2022 at 19:33):

@Ali Caglayan I followed these steps and removed the snap package and now everything is working. Thank you for the instructions.

view this post on Zulip Notification Bot (Jan 25 2022 at 19:34):

Ali Caglayan has marked this topic as resolved.

Last updated: Oct 13 2024 at 01:02 UTC