We recommend installation using opam if you wish to install the HoTT library to use in your own project or to play around with.

• 1. Using the HoTT library
• 2. Installation of HoTT library using opam
  • Released Versions
  • Source Versions
  • Development Versions
• 3. Setup for developers (using git)
  • 3.1. Prerequisites (Installing Rocq)
    • 3.1.1. Development in OSX and Windows
  • 3.2. Forking and obtaining the HoTT library
  • 3.3. Building the HoTT library
  • 3.4. Installing the library using git
• 4. Editors
  • 4.1. Tags for Emacs
• 5. Updating the library
• 6. Troubleshooting

In order to use the HoTT library in your project, make sure you have a file called _CoqProject in your working directory which contains the following lines:

-arg -noinit
-arg -indices-matter

This way when you open .v files using rocqide or any other text editor for Rocq (see Editors), the editor will pass the correct arguments to Rocq.

To import modules from the HoTT library inside your own file, you will need to write the following:

From HoTT Require Import Basics.

This, for example, will import the Basics module from the HoTT library. If you wish to import the entire library you can write:

From HoTT Require Import HoTT.

To install the HoTT library via opam, first install opam and add the released Rocq opam archive as follows:

$ opam repo add rocq-released https://rocq-prover.org/opam/released

This will let you install the released versions of the library. We typically do a release for each major version of Rocq. The opam package is still named coq-hott.

$ opam install coq-hott

After cloning the repository, you can install the library using opam by running opam install . in the root of the repository.

We also have the current development version of the library available via opam. Add the development repositories and install the package as follows:

$ opam repo add rocq-core-dev https://rocq-prover.org/opam/core-dev
$ opam repo add rocq-extra-dev https://rocq-prover.org/opam/extra-dev
$ opam install coq-hott.dev

The coq-hott.dev package requires the development version of Rocq. To use a released version of Rocq with the library's current sources, follow the Source Versions instructions instead.

The required Rocq and Dune versions are listed in the package dependencies. We recommend that you use the opam package manager to install Rocq. Details about installing Opam can be found here. We also recommend working within an opam switch, to keep your work isolated from other packages installed via opam.

After setting up a switch (if you choose to do so), install Rocq with:

$ opam install rocq-core

You will also need make and git in a typical workflow. For Dune builds, install Dune with opam install dune.

We don't recommend developing on platforms other than Linux, however it is still possible.

Windows and OSX users can find additional setup instructions in the Rocq installation guide.

For OSX users git and make should be readily available.

Windows users can install git as described here and make as described here.

In order to do development on the HoTT library, we recommend that you fork it on Github. More details about forking can be found here.

Use git to clone your fork locally:

$ git clone https://github.com/YOUR-USERNAME/HoTT

Of course, you may clone the library directly, but for development it is recommended to work on a fork.

To follow the rest of the instructions, it is best to change your working directory to the HoTT directory.

$ cd HoTT

We also recommend that you add the main repository as a git remote. This makes it easier to track changes happening on the main repository. This can be done as follows:

$ git remote add upstream https://github.com/HoTT/HoTT.git

In order to compile the files of the HoTT library, run make:

$ make

You can speed up the build by passing -jN where N is the number of parallel recipes make will execute.

You can also use dune to build the library.

$ dune build

When developing HoTT itself, build in the checkout; installation is not needed. To use your checkout from a separate project, install it with:

$ make install

We recommend the following text editors for the development of .v files:

• Emacs together with Proof General.
• RocqIDE part of the Rocq Proof Assistant.
• Visual Studio Code together with coq-lsp.
• For more editors, see the Rocq website's installation guide.

To use the Emacs tags facility with the *.v files here, run the command:

$ make TAGS

The Emacs command M-x find-tag, bound to M-. , will take you to a definition or theorem, the default name for which is located under your cursor. Read the help on that Emacs command with C-h k M-. , and learn the other facilities provided, such as the use of M-* to get back where you were, or the use of M-x tags-search to search throughout the code for locations matching a given regular expression.

Dune users may use the following to generate tags:

dune build TAGS

If you installed the library via opam then simply run opam update and then opam upgrade.

To upgrade your clone of the GitHub repository as set up in the instructions on using git: Pull the latest version using git pull upstream master and then rebuild using make as above.

To update your fork, use git push origin master. We also have tags in the GitHub repository for our released versions which you can use instead of master.

In case of any problems, feel free to contact us by opening an issue on GitHub.