|
| 1 | +--- |
| 2 | +kind: rocq |
| 3 | +version: 9.0+rc1 |
| 4 | +date: 2025-01-24 |
| 5 | +is_latest: true |
| 6 | +is_lts: false |
| 7 | +intro: | |
| 8 | + This page describes Rocq version **9.0+rc1**, released on |
| 9 | + Jan 24, 2025. Go [here](/releases) for a list of all releases. |
| 10 | +
|
| 11 | + This is the first release candidate of Rocq 9. |
| 12 | +highlights: | |
| 13 | + - A single command line tool: `rocq` |
| 14 | + - Compatibility Coq binaries and packages |
| 15 | + - Improvements to template and sort polymorphism |
| 16 | + - Support for quick fixes in LSP-based interfaces (e.g. for deprecations) |
| 17 | +--- |
| 18 | + |
| 19 | +## Changes |
| 20 | + |
| 21 | +See the full [changelog](https://coq.inria.fr/doc/V9.0+rc1/refman/changes.html#changes-in-9-0-0) in the reference manual. |
| 22 | + |
| 23 | +## Installation Instructions |
| 24 | + |
| 25 | +The base proof assistant can be installed as an opam switch with the following commands: |
| 26 | +```bash |
| 27 | +opam update |
| 28 | +opam switch create 4.14.1 |
| 29 | +opam repo add coq-core-dev https://coq.inria.fr/opam/core-dev |
| 30 | +opam install rocq-prover.9.0+rc1 |
| 31 | +``` |
| 32 | + |
| 33 | +Refer to the [general install instructions](/docs/installing-rocq) for more information. |
| 34 | + |
| 35 | +Source Distribution |
| 36 | +------------------- |
| 37 | + |
| 38 | +- [Source |
| 39 | + tarball](https://github.com/coq/coq/archive/refs/tags/V9.0+rc1.tar.gz) |
| 40 | + (`.tar.gz`) for compilation under Unix (including Linux and macOS X) |
| 41 | + and Microsoft Windows (including Cygwin). |
| 42 | +- Also available in |
| 43 | + [`.zip`](https://github.com/coq/coq/archive/refs/tags/V9.0+rc1.zip) |
| 44 | + format. |
| 45 | +- [Opam](https://opam.ocaml.org/) is a source-based distribution of |
| 46 | + OCaml, Rocq and many companion libraries and tools. Compilation and |
| 47 | + installation are automated by powerful package managers. |
| 48 | +- The official development repo is hosted on |
| 49 | + [GitHub](https://github.com/coq/coq). |
| 50 | + |
0 commit comments