Skip to content

Briefly mention Rocq in INSTALL.md #2321

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
jdchristensen merged 2 commits into from
Nov 7, 2025
+24 −3
Merged

Briefly mention Rocq in INSTALL.md #2321

Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
38e02cb
Briefly mention Rocq in INSTALL.md
jdchristensen Nov 4, 2025
67669e9
INSTALL.md: fix typo
jdchristensen Nov 6, 2025
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
27 changes: 24 additions & 3 deletions INSTALL.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -9,7 +9,7 @@ library to use in your own project or to play around with.
- [Source Versions](#source-versions)
- [Development Versions](#development-versions)
- [3. Setup for developers (using git)](#3-setup-for-developers-using-git)
- [3.1. Prequisites (Installing Coq)](#31-prequisites-installing-coq)
- [3.1. Prerequisites (Installing Coq)](#31-prerequisites-installing-coq)
- [3.1.1. Development in OSX and Windows](#311-development-in-osx-and-windows)
- [3.2. Forking and obtaining the HoTT library](#32-forking-and-obtaining-the-hott-library)
- [3.3. Building the HoTT library](#33-building-the-hott-library)
Expand All @@ -21,6 +21,11 @@ library to use in your own project or to play around with.

# 1. Installation using Coq Platform

**Note:** As of version 9.0, Coq has been renamed Rocq. When you install Coq-HoTT
following the instructions in this section, it should automatically
install the compatibility wrappers, so that the nothing about the build process
needs to change.

In order to install the HoTT library, we recommend that you use the [Coq
Platform][1]. This will install the [Coq Proof Assistant][2] together with the
HoTT library. The Coq Platform supports installation on **Linux**, **MacOS** and
Expand Down Expand Up @@ -63,6 +68,11 @@ From HoTT Require Import HoTT.

# 2. Installation of HoTT library using opam

**Note:** As of version 9.0, Coq has been renamed Rocq. When you install Coq-HoTT
following the instructions in this section, it should automatically
install the compatibility wrappers, so that the nothing about the build process
needs to change.

## Released Versions

More advanced users may wish to install the HoTT library via `opam` ([See here
Expand Down Expand Up @@ -99,17 +109,26 @@ Then install the library with `opam install coq-hott`, as for the released versi

# 3. Setup for developers (using git)

## 3.1. Prequisites (Installing Coq)
## 3.1. Prerequisites (Installing Coq)

We recommend that you use the `opam` package manager to install `coq`. Details
about [installing Opam can be found here][3].
We also recommend working within an [opam switch][20], to keep your work
isolated from other packages installed via opam.

Using `opam` you can install the latest version of `coq` by doing the following:
After setting up a switch (if you choose to do so),
you can install the latest 8.x version of `coq` by doing the following:

```shell
$ opam install coq
```

To install the latest 9.x version of Rocq and the Coq compatibility wrappers, do

```shell
$ opam install rocq-core coq-core
```

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


Expand Down Expand Up @@ -252,3 +271,5 @@ GitHub](https://github.com/HoTT/HoTT).
[17]: https://stackoverflow.com/a/54086635
[18]: https://git-scm.com/book/en/v2/Getting-Started-Installing-Git
[19]: https://coq.inria.fr/user-interfaces.html

[20]: https://ocaml.org/docs/opam-switch-introduction
Loading