coqcoq-tacticformal-verificationformal-methodscoqide

How to Import Coq library HoTT in CoqIde

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?
Solution

  • 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.