How to Import Coq library HoTT in CoqIde

Question

I want to use HoTT library in my CoqIde. My environment is Coq_Platform_2021.09.0.8.13-installer-windows-x86_64-signed and I have tried a lot of methods.

1. I tried to write Require Import HoTT. in CoqIde and get the error Unable to locate library HoTT. (While searching for a .vos file.)
2. I tried to write From HoTT Require Import Basics. or Require Import HoTT.Basics. and I get the error Notation "~ _" is already defined at level 75 with arguments constr at level 75
3. However, I can load some libraries such as UnivalenceAxiom by writing From HoTT Require Import UnivalenceAxiom. So my question is how to import HoTT library in my CoqIde?

Answer 1

You need to put a file named _CoqProject with the following contents:

-arg -noinit
-arg -indices-matter

In your project root folder (from which you load the file using HoTT).

It would help if you could tell us the places where you looked for documentation on this, so that we can adjust it. It is e.g. documented in opam (say if you do opam show coq-hott), but I guess this is not the most obvious place to look fot his.

Answer 2

I had this exact same issue and "fixed" it by adding this line to the top of my file, before importing HoTT: Reserved Notation "~ x" (at level 35, right associativity).

So my entire file looked like:

Reserved Notation "~ x" (at level 35, right associativity).
From HoTT Require Import HoTT.

And it worked fine from there on. Confusingly, Emacs highlighted the notation line as an error, yet it loads fine and I can continue onwards. IMO this seems like a bug with more recent versions of Coq.