The release management team for Coq 8.10 is proud and happy to launch the first β-testing phase for the next major version of Coq.
Coq version 8.10 contains two major new features: support for a native machine integer type and a new sort SProp, a definitionally proof irrelevant universe. It is also the result of refinements and stabilization of previous features, deprecations or removals of deprecated features, cleanups of the internals of the system and API, and many documentation improvements. This release includes many user-visible changes, including deprecations and new features. A more detailed list of changes appears in the reference manual.
You can find the source code for that version on the git repository https://github.com/coq/coq/releases/tag/V8.10%2Bbeta1. Installers for Windows and macOS are also available there. Pre-built binary for Linux can be obtained through cachix.
Please try out this new version, package it for your favorite distribution, release your own plug-ins and libraries… and report the bugs and issues that you may encounter on the bug tracker
(https://github.com/coq/coq/issues).
Caveat: at the time of this writing, there are two known significant issues. You may get more information about them and track the work towards their resolution on the corresponding threads:
- CoqIDE does not work properly on Windows (issue #9885);
- Template polymorphism breaks Prop/Set separation (issue #9294, proposed fix).
Happy testing!