CODEWITHSUNDEEP
coqcoq-tacticformal-verificationformal-methodscoqide
Huan Sun
Huan Sun

Reputation: 167

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?

Upvotes: 0

Views: 248

Answers (2)

Dessertion
Dessertion

Reputation: 1

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.

Upvotes: 0

M Soegtrop
M Soegtrop

Reputation: 1448

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.

Upvotes: 2

Related Questions