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?
Do you get the message in coqide?
Did you start coqide in the same directory as your _CoqProject?
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.
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
opam repo add coq-released https://coq.inria.fr/opam/released
for released versions of HoTT (there should be one for each released version of coq)
opam repo add coq-extra-dev https://coq.inria.fr/opam/extra-dev if you are using coq master
opam install coq-hott should install HoTT properly
extra-dev opam repo if possible, and in general Coq
master can be hard to use)
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.
@Ali Caglayan I followed these steps and removed the snap package and now everything is working. Thank you for the instructions.
Ali Caglayan has marked this topic as resolved.
Last updated: Oct 01 2023 at 18:01 UTC