Skip to content

INSTALL.md

Latest commit

 

History

History
254 lines (188 loc) · 8.45 KB

INSTALL.md

File metadata and controls

254 lines (188 loc) · 8.45 KB
Raw

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

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.

Warning

The versions of the HoTT library appearing in the Coq Platform are released twice a year. This means that there is a good chance that the Coq Platform version is lagging behind the latest version of the library. If you wish to use the latest version of the library, you should install it using opam as described in the next section.

2. Installation of HoTT library using opam

Released Versions

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

Source Versions

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

Development Versions

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-core-dev https://coq.inria.fr/opam/core-dev
$ opam repo add coq-extra-dev https://coq.inria.fr/opam/extra-dev

This will make coq.dev the latest available version of coq. You can pin coq to a stable version by running opam pin add coq.dev 8.19.1 for example. Then install the library with opam install coq-hott, as for the released version.

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:

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.