INSTALL.md

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

Table of contents

• 1. Installation using Coq Platform
• 2. Installation of HoTT library using opam
• 3. Setup for developers (using git)
  • 3.1. Prequisites (Installing Coq)
    • 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

1. Installation using Coq Platform

In order to install the HoTT library, we recommend that you use the Coq Platform. This will install the Coq Proof Assistant together with the HoTT library. The Coq Platform supports installation on Linux, MacOS and Windows.

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 coqide or any other text editor for coq (see Editors), the editor will pass the correct arguments to coq.

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.

2. Installation of HoTT library using opam

More advanced users may wish to install the HoTT library via opam (See here for details on installing opam). You need to add the released coq-archive packages to opam which can be done as follows:

$ opam repo add coq-released https://coq.inria.fr/opam/released

This will let you install the released versions of the library. We typically do a release for each major version of coq. Note that the name of the HoTT library is coq-hott inside the coq-archive.

$ opam install coq-hott

We also have the current development versions of the library available via opam. For this however, you will need to add the dev coq-archive packages:

$ opam repo add coq-extra-dev https://coq.inria.fr/opam/extra-dev

3. Setup for developers (using git)

3.1. Prequisites (Installing Coq)

We recommend that you use the opam package manager to install coq. Details about installing Opam can be found here.

Using opam you can install the latest version of coq by doing the following:

$ opam install coq

You will also need make and git in a typical workflow.

3.1.1. Development in OSX and Windows

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

Windows and OSX users may install coq directly using the installer for the appropriate coq release.

For OSX users git and make should be readily availble.

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

3.2. Forking and obtaining the HoTT library

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

3.3. Building the HoTT library

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

3.4. Installing the library using git

We don't recommend you install the library using the repository and instead recommend installing via opam, especially if you are intending to develop the library. However the makefile contains a target called install and therefore running

$ make install

will install the library.

4. Editors

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

• Emacs together with Proof General.
• CoqIDE part of the Coq Proof Assistant.
• Visual Studio Code together with VSCoq.

4.1. Tags for Emacs

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

5. Updating the library

If you installed the library via Coq Platform then update your version of Coq Platform.

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

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.

6. Troubleshooting

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