2023.11.0 with latest pick Coq 8.18.0~2023.11 and 8.18.0~mc2

Recommended binary installers

• Windows (64 bit) installer for Coq 8.18.0 with MathComp 1.18 (default)
• Windows (64 bit) installer for Coq 8.18.0 with MathComp 2.1 (incomplete)
• MacOS (arm) installer for Coq 8.18.0 with MathComp 1.18 (default)
• MacOS (arm) installer for Coq 8.18.0 with MathComp 2.1 (incomplete)
• MacOS (intel) installer for Coq 8.18.0 with MathComp 1.18 (default)
• MacOS (intel) installer for Coq 8.18.0 with MathComp 2.1 (incomplete)
• Linux (Snap) installer for Coq 8.18.0

General information

See README for general information and installation of Coq Platform.

See Charter for the concept and goals of Coq Platform.

See CEP52 for the Coq and Coq Platform release cycle.

See macOS, Linux and Windows for detailed installation and usage instructions.

Major enhancements

Two release package picks for Coq 8.18.0 are included with an updated package list. No new packages have been added - this will be done in a soon to follow minor release. The two releases support MathComp 1.18 and MathComp 2.1 respectively. The reasons for providing two picks this time are that it might be a larger step to move from MC 1.18 to 2.1 and because, at the time of picking, one package (mathcomp-analysis) was not yet ported to MC 2.1 (it is at time of this release).

• See the Coq 8.18 release notes for the changes in Coq.
• See README~8.18~2023.11.md for a full description of the MC 1.18 based package pick.
• See README~8.18~mc2.md for a full description of the MC 2 based package pick.

Included Versions of Coq

Recommended Coq version

• Coq 8.18.0 with 2023.11 MathComp 1.18 based release package collection
• Coq 8.18.0 with 2023.11 MathComp 2.1 based release package collection

Compatibility Coq versions

The compatibility versions are intended to help porting packages from an older to the latest release. They can be installed in parallel with other versions of Coq (Coq Platform will create separate opam switches for each Coq version).

• Coq 8.17.1 with the first package collection from August 2023
• Coq 8.16.1 with an updated package collection from August 2023 which is as much as possible compatible with the first 8.17.1 package collection
• Coq 8.16.1 with the first package collection from September 2022
• Coq 8.15.2 with an updated package collection from September 2022 which is as much as possible compatible as possible with the first 8.16.1 package collection
• Coq 8.15.2 with the first package collection from April 2022
• Coq 8.14.1 with an updated package collection from April 2022 which is as much as possible compatible as possible with the first 8.15.2 package collection
• Coq 8.14.1 with the first package collection from January 2022
• Coq 8.13.2 with an updated package collection from January 2022 which is as much as possible compatible as possible with the first 8.14.1 package collection
• Coq 8.13.2 with an updated package collection from September 2021
• Coq 8.13.2 with the original package collection from February 2021
• Coq 8.12.2 with the same package collection as the 8.12.2 Coq Platform release

Only the 8.18.0 version with the MC 1.18 and MC 2.1 based package collections are available as installers for macOS and Windows and Snap package. Other versions can be installed using the Coq Platform scripts or the binary installers from previous Platform releases.

Notes

• Notes on the macOS installer: Because the application is signed but not "notarized", it won't open by default, unless you right-click the application in Finder and chose Open. Cf. #51 to learn more. The installer is now designed to be compatible down to macOS 10.13, but this is not much tested. We appreciate bug reports for 10.X macOS versions, but we will ask you for help fixing them.

• Notes on Apple ARM silicon: Coq Platform is now fully supported on Apple ARM silicon.

• Notes on Windows Cygwin environment: In the Cygwin setup created by the "compile from sources" scripts on Windows, the path structure changed, so that packages relying on dune - which tends to use rather long paths for intermediate files - work better. The opam root path is now /opam instead of /home/<user>/.opam. This saves some 10 characters and notably makes the path name independent of the user name. The platform root folder is now /platform instead of /home/<user>/platform.

• Notes on CoqHammer: The proof generation component of CoqHammer is available on macOS and Linux only. The CoqHammer tactics, which reconstruct generated proofs, do work on Windows, though. Since the CoqHammer tactic running on macOS and Linux creates simple and fast Coq tactic call snippets which are intended to replace the slow generator tactics, it is possible to use the auto generated tactics on Windows as well. Also you can manually write CoqHammer tactic calls on Windows.

• Note on QuickChick: QuickChick requires an OCaml compiler to run. The binary installers for Coq Platform do not provide OCaml, so QuickChick does not work with the binary installers for macOS, Windows and Snap. It is recommended to use the "compile from sources" method if you want to use QuickChick. An alternative method is to install OCaml by other means and have it in the PATH, but this method is not supported by the Coq Platform team. We plan to add an OCaml compiler to the binary installers in a future release.

• Note on SerAPI: The SerAPI executables like sertop require that either the COQLIB environment variable is exported or a --coqlib=${coqc -where} or similar option is given. Other Coq tools like coqc determine the Coq library path from the binary location, but sertop does not (yet).

• Note on SerAPI on Windows: The package has been added back on Windows after some restructuring of paths (see above)

• Note on coq_makefile on Windows: The Windows installers don't supply make because make is quite limited without a posix shell. An addon is supplied which contains a Windows native gnumake and a patched template file for coq_makefile which allows to use coq_makefile and gnumake with CMD as shell.

Installers

Binary installers are provided for the 2023.11 and mc2 pick for Coq 8.18.0. The Windows installers can be downloaded below. The MacOS installers and snap packages are still in signing / publishing and will be available soon.

2023.03.0/.1 with latest pick Coq 8.17.1~2023.08

Recommended binary installers

• Windows (64 bit) installer for Coq 8.17.1
• macOS (Intel) installer for Coq 8.17.1
• macOS (M1/M2/Apple Silicon/ARM) installer for Coq 8.17.1
• Linux (Snap) installer for Coq 8.17.1

General information

See README for general information and installation of Coq Platform.

See Charter for the concept and goals of Coq Platform.

See CEP52 for the Coq and Coq Platform release cycle.

See macOS, Linux and Windows for detailed installation and usage instructions.

Major enhancements

A release package pick for Coq 8.17.1 is included with an updated package list (no new packages have been added).

• See the Coq 8.17 release notes for the changes in Coq.
• See README~8.17~2023.08.md for a full description of the new package pick.

Included Versions of Coq

Recommended Coq version

• Coq 8.17.1 with 2023.08 release package collection

Compatibility Coq versions

The compatibility versions are intended to help porting packages from an older to the latest release. They can be installed in parallel with other versions of Coq (Coq Platform will create separate opam switches for each Coq version).

• Coq 8.16.1 with an updated package collection which is as much as possible compatible with the new 8.17.1 release package pick
• Coq 8.16.1 with the first package collection from September 2022
• Coq 8.15.2 with an updated package collection from September 2022 - this package pick is made to be as compatible as possible with the first 8.16.1 package collection
• Coq 8.15.2 with the first package collection from April 2022
• Coq 8.14.1 with an updated package collection from April 2022 - this package pick is made to be as compatible as possible with the 8.15.2 package collection
• Coq 8.14.1 with the first package collection from January 2022
• Coq 8.13.2 with an updated package collection from January 2022 - this package pick is made to be as compatible as possible with the first 8.14.1 package collection
• Coq 8.13.2 with an updated package collection from September 2021
• Coq 8.13.2 with the original package collection from February 2021
• Coq 8.12.2 with the same package collection as the 8.12.2 Coq Platform release

Only the 8.17.1 version with the new 2023.08 package collection is available as installer for macOS and Windows and Snap package. Other versions can be installed using the Coq Platform scripts or the binary installers from previous Platform releases.

Notes

• Note on bugfix release 2023.03.1: this bugfix release only applies to snap. The snap release has been updated. Since Windows and macOS are not affected, the original 2023.03.0 installers are kept.

• Notes on the macOS installer: Because the application is signed but not "notarized", it won't open by default, unless you right-click the application in Finder and chose Open. Cf. #51 to learn more. The installer is now designed to be compatible down to macOS 10.13, but this is not much tested. We appreciate bug reports for 10.X macOS versions, but we will ask you for help fixing them.

• Notes on Apple ARM silicon: Coq Platform has been tested by users on Apple silicon (M1), but we have no means to run CI tests on Apple silicon (yet), so this is not officially supported. We appreciate bug reports for Apple silicon, but we will ask you for help fixing them.

• Notes on CoqHammer: The proof generation component of CoqHammer is available on macOS and Linux only. The CoqHammer tactics, which reconstruct generated proofs, do work on Windows, though. Since the CoqHammer tactic running on macOS and Linux creates simple and fast Coq tactic call snippets which are intended to replace the slow generator tactics, it is possible to use the auto generated tactics on Windows as well. Also you can manually write CoqHammer tactic calls (that is, use it as replacement for auto) on Windows.

• Note on QuickChick: QuickChick requires an OCaml compiler to run. The binary installers for Coq Platform do not provide OCaml, so QuickChick does not work with the binary installers for macOS, Windows and Snap. It is recommended to use the "compile from sources" method if you want to use QuickChick. An alternative method is to install OCaml by other means and have it in the PATH, but this method is not supported by the Coq Platform team. We plan to add an OCaml compiler to the binary installers in a future release.

• Note on SerAPI: The SerAPI executables like sertop require that either the COQLIB environment variable is exported or a --coqlib=${coqc -where} or similar option is given. Other Coq tools like coqc determine the Coq library path from the binary location, but sertop does not (yet).

• Note on SerAPI on Windows: The package is currently not included on Windows cause of path length issues. One can build it if one is careful about the length of the root path (C:\bin\cygwincoq works if the Windows user name is no more than 10 characters)

• Note on coq_makefile on Windows: The Windows installers don't supply make because make is quite limited without a posix shell. An addon is supplied which contains a Windows native gnumake and a patched template file for coq_makefile which allows to use coq_makefile and gnumake with CMD as shell.

Installers

Binary installers are provided for the 2023.08 pick of Coq 8.17.1 for macOS, Windows and Linux (snap). The macOS and Windows installers can be downloaded below. The snap package is available via snapcraft.

2022.09.1

Recommended binary installers

• Windows (64 bit) installer for Coq 8.16
• macOS (Intel) installer for Coq 8.16
• macOS (M1/M2/Apple Silicon/ARM) installer for Coq 8.16
• Linux (Snap) installer for Coq 8.16

General information

See README for general information and installation of Coq Platform.

See Charter for the concept and goals of Coq Platform.

See CEP52 for the Coq and Coq Platform release cycle.

See macOS, Linux and Windows for detailed installation and usage instructions.

Major enhancements

A release package pick for Coq 8.16.1 is included with an updated and substantially extended package list.

• See the Coq 8.16 release notes for the changes in Coq.
• See README~8.16~2022.09.md for a full description of the new package pick.

This is the first Coq Platform release which contains a MacOS "M1 / M2 / Apple silicon / ARM" DMG installer (see link above). This doesn't mean it is fully supported as yet since we still don't have CI for MacOS ARM, but it should be pretty solid. An ARM DMG installer for Coq 8.15.2 with the 2022.09 pick is also included.

These packages have been added to the "full" level in the 2022.09 pick:

• coq-itauto.8.16.0
• coq-mathcomp-algebra-tactics.1.0.0 (moved from "extended")
• coq-mathcomp-word.1.1

These packages have been added to the "extended" level in the 2022.09 pick:

• coq-metacoq.1.1+8.16
• coq-fiat-crypto.0.0.15
• coq-bedrock2.0.0.3
• coq-bedrock2-compiler.0.0.3
• coq-rupicola.0.0.5
• coq-coqutil.0.0.2
• coq-rewriter.0.0.6
• coq-riscv.0.0.2

Caveats

• From Coq 8.16.0 on, Coq uses Ocamlfind to find shared libraries used by coq tools and plugins. Ocamlfind has not been designed with installers and relocation in mind - that is, using software in a different place than it was compiled in. Some patching was done to Ocamlfind by the Coq Platform team to make the installers work. This is well tested, but please have an eye on plugins and report issues.

Included Versions of Coq

Recommended Coq version

• Coq 8.16.1 with 2022.09 release package collection

Compatibility Coq versions

The compatibility versions are intended to help porting packages from an older to the latest release. They can be installed in parallel with other versions of Coq (Coq Platform will create separate opam switches for each Coq version).

• Coq 8.15.2 with an updated package collection which is as much as possible compatible with the new 8.16.1 release package pick
• Coq 8.15.2 with the first package collection from April 2022
• Coq 8.14.1 with an updated package collection from April 2022 - this package pick is made to be as compatible as possible with the 8.15.2 package collection
• Coq 8.14.1 with the first package collection from January 2022
• Coq 8.13.2 with an updated package collection from January 2022 - this package pick is made to be as compatible as possible with the first 8.14.1 package collection
• Coq 8.13.2 with an updated package collection from September 2021
• Coq 8.13.2 with the original package collection from February 2021
• Coq 8.12.2 with the same package collection as the 8.12.2 Coq Platform release

Only the 8.16.1 and 8.15.2 versions with the new 2022.09 package collection are available as installers for macOS and Windows and only the 8.16.1 version as a Snap package. Other versions can be installed using the Coq Platform scripts or the binary installers from previous Platform releases.

Notes

• Notes on the macOS installer: Because the application is signed but not "notarized", it won't open by default, unless you right-click the application in Finder and chose Open. Cf. #51 to learn more. The installer is now designed to be compatible down to macOS 10.13, but this is not much tested. We appreciate bug reports for 10.X macOS versions, but we will ask you for help fixing them.

• Notes on Apple ARM silicon: Coq Platform has been tested by users on Apple silicon (M1), but we have no means to run CI tests on Apple silicon (yet), so this is not officially supported. We appreciate bug reports for Apple silicon, but we will ask you for help fixing them. Note that the macOS ARM installers have been rebuilt after the release tag to fix a bug in the installer creation script.

• Notes on CoqHammer: The proof generation component of CoqHammer is available on macOS and Linux only. The CoqHammer tactics, which reconstruct generated proofs, do work on Windows, though. Since the CoqHammer tactic running on macOS and Linux creates simple and fast Coq tactic call snippets which are intended to replace the slow generator tactics, it is possible to use the auto generated tactics on Windows as well. Also you can manually write CoqHammer tactic calls (that is, use it as replacement for auto) on Windows.

• Note on QuickChick: QuickChick requires an OCaml compiler to run. The binary installers for Coq Platform do not provide OCaml, so QuickChick does not work with the binary installers for macOS, Windows and Snap. It is recommended to use the "compile from sources" method if you want to use QuickChick. An alternative method is to install OCaml by other means and have it in the PATH, but this method is not supported by the Coq Platform team. We plan to add an OCaml compiler to the binary installers in the next release.

• Note on SerAPI: The SerAPI executables like sertop require that either the COQLIB environment variable is exported or a --coqlib=${coqc -where} or similar option is given. Other Coq tools like coqc determine the Coq library path from the binary location, but sertop does not (yet).

• Note on coq_makefile on Windows: The Windows installers don't supply make because make is quite limited without a posix shell. An addon is supplied which contains a Windows native gnumake and a patched template file for coq_makefile which allows to use coq_makefile and gnumake with CMD as shell.

Installers

Binary installers are provided for the 2022.09 pick of Coq 8.16.1 and 8.15.2 for macOS, Windows and Linux (snap, only for Coq 8.16.1). The macOS and Windows installers can be downloaded below. The snap package is available via snapcraft.

2022.09.0 with Coq 8.16.0 and beta package collection

Recommended binary installers

• Beta Windows (64 bit) installer for Coq 8.16
• Beta macOS installer for Coq 8.16
• Beta Linux (Snap) installer for Coq 8.16 - coming soon

General information

See README for general information and installation of Coq Platform.

See Charter for the concept and goals of Coq Platform.

See CEP52 for the Coq and Coq Platform release cycle.

See macOS, Linux and Windows for detailed installation and usage instructions.

Major enhancements

A beta package pick for Coq 8.16.0 is included with an updated and substantially extended package list.

• See the Coq 8.16 release notes for the changes in Coq.
• See 8.16~2022.09~beta1 for a full description of the new package pick.

These packages have been added to the "full" level in the 2022.09 pick:

• coq-itauto.8.16.0
• coq-mathcomp-algebra-tactics.1.0.0 (moved from "extended")
• coq-mathcomp-word.1.1

These packages have been added to the "extended" level in the 2022.09 pick:

• coq-metacoq.1.1+8.16
• coq-fiat-crypto.0.0.15
• coq-bedrock2.0.0.3
• coq-bedrock2-compiler.0.0.3
• coq-rupicola.0.0.5
• coq-coqutil.0.0.2
• coq-rewriter.0.0.6
• coq-riscv.0.0.2

Things to have an eye on in the beta releases

This Coq Platform release contains a macOS/Snap/Windows installers for 8.16.0 with a beta package pick. If you try these beta installers, we would like you to have an eye on the following points:

• With Coq 8.16.0, Coq uses Ocamlfind to find shared libraries. Ocamlfind has not been designed with installers and relocation in mind - that is, using software in a different place than it was compiled in. Some patching was done to Ocamlfind by the Coq Platform team to make the installers work. To test this, please have a look at all your favorite plugins.
• There are two patches to CoqIDE included, which are not in the 8.16.0 release:
  • Fix "Interrupt computations" on Windows (Windows specific)
  • IDE crashed when trying to do edit->preferences (macOS specific)

Included Versions of Coq

Recommended Coq version

• Coq 8.16.0 with a beta package collection

Compatibility Coq versions

The compatibility versions are intended to help porting packages from an older to the latest release. They can be installed in parallel with other versions of Coq (Coq Platform will create separate opam switches for each Coq version).

• Coq 8.15.2 with an updated package collection which is as much as possible compatible with the new 8.16.0 beta package pick
• Coq 8.15.2 with the first package collection from April 2022
• Coq 8.14.1 with an updated package collection from April 2022 - this package pick is made to be as compatible as possible with the 8.15.2 package collection
• Coq 8.14.1 with the first package collection from January 2022
• Coq 8.13.2 with an updated package collection from January 2022 - this package pick is made to be as compatible as possible with the first 8.14.1 package collection
• Coq 8.13.2 with an updated package collection from September 2021
• Coq 8.13.2 with the original package collection from February 2021
• Coq 8.12.2 with the same package collection as the 8.12.2 Coq Platform release

Only the 8.16.0 and 8.15.2 versions with the new (beta) package collection are available as installers for macOS and Windows and only the 8.16.0 version as a Snap package. Other versions can be installed using the Coq Platform scripts or the binary installers from previous Platform releases.

Notes

• Notes on compiling from sources on Windows: If you compile from sources on Windows, please use main instead of the tag - the tag has build issues caused by changes in opam.

• Notes on the macOS installer: Because the application is signed but not "notarized", it won't open by default, unless you right-click the application in Finder and chose Open. Cf. #51 to learn more. The installer is now designed to be compatible down to macOS 10.13, but this is not much tested. We appreciate bug reports for 10.X macOS versions, but we will ask you for help fixing them.

• Notes on Apple ARM silicon: Coq Platform has been tested by users on Apple silicon (M1), but we have no means to run CI tests on Apple silicon (yet), so this is not officially supported. We appreciate bug reports for Apple silicon, but we will ask you for help fixing them.

• Notes on CoqHammer: The proof generation component of CoqHammer is available on macOS and Linux only. The CoqHammer tactics, which reconstruct generated proofs, do work on Windows, though. Since the CoqHammer tactic running on macOS and Linux creates simple and fast Coq tactic call snippets which are intended to replace the slow generator tactics, it is possible to use the auto generated tactics on Windows as well. Also you can manually write CoqHammer tactic calls (that is use it as replacement for auto) on Windows.

• Note on QuickChick: QuickChick requires an OCaml compiler to run. The binary installers for Coq Platform do not provide OCaml, so QuickChick does not work with the binary installers for macOS, Windows and Snap. It is recommended to use the "compile from sources" method if you want to use QuickChick. An alternative method is to install OCaml by other means and have it in the PATH, but this method is not supported by the Coq Platform team. We plan to add an OCaml compiler to the binary installers in the next release.

• Note on Serapi: The SerAPI executables like sertop require a --coqlib=${coqc -where} or similar option. The `COQLIB environment variable is not used.

Installers

Binary installers are provided for the 2022.09~beta1 pick of Coq 8.16.0 for macOS, Windows and Linux (snap). The macOS and Windows installers can be downloaded below. The snap package will be available soon via snapcraft.

2022.04.1

Recommended binary installers

• Windows (64 bit) installer for Coq 8.15
• macOS installer for Coq 8.15
• Linux (Snap) installer for Coq 8.15

General information

See README for general information and installation of Coq Platform.

See Charter for the concept and goals of Coq Platform.

See CEP52 for the Coq and Coq Platform release cycle.

Major enhancements

The latest release version of Coq has been updated from 8.15.1 to 8.15.2 (see Coq 8.15.2 release notes). This is a bug fix release with a few important fixes:

• Various issues introduced in CoqIDE by the implementation of the Ltac Debugger have been fixed, most notably a quadratic blow up in parsing time.
• A wrong standard library axiom for the native float implementation allowed a proof of false.

Included Versions of Coq

Recommended Coq version

• Coq 8.15.2 with the same package collection as the 2022.04.0 release.

Compatibility Coq versions

The compatibility versions are intended to help porting packages from an older to the latest release. They can be installed in parallel with other versions of Coq (Coq Platform will create separate opam switches for each Coq version).

• Coq 8.14.1 with an updated package collection from Apr 2022 - this package pick is made to be as compatible as possible with the 8.15.2 package collection
• Coq 8.14.1 with the first package collection from Jan 2022
• Coq 8.13.2 with an updated package collection from January 2022 - this package pick is made to be as compatible as possible with the first 8.14.1 package collection
• Coq 8.13.2 with an updated package collection from September 2021
• Coq 8.13.2 with the original package collection from February 2021
• Coq 8.12.2 with the same package collection as the 8.12.2 Coq Platform release

Only the 8.14.1 and the 8.15.2 version are available as installers for macOS and Windows and only the 8.15.2 version as snap package. Other versions can be installed using the Coq Platform scripts.

Notes

• Notes on the macOS installer: This installer is only compatible with macOS 11.0 or higher. Because the application is signed but not "notarized", it won't open by default, unless you right-click the application in Finder and chose Open. Cf. #51 to learn more.

• Notes on Apple ARM silicon: Coq Platform has been tested by users on Apple silicon (M1), but we have no means to run CI tests on Apple silicon (yet), so this not officially supported. We appreciate bug reports for Apple silicon, but we will ask you for help fixing them.

• Notes on CoqHammer: The proof generation component of CoqHammer is available on macOS and Linux only. The CoqHammer tactics, which reconstruct generated proofs, do work on Windows, though. Since the CoqHammer tactic running on macOS and Linux creates simple and fast Coq tactic call snippets which are intended to replace the slow generator tactics, it is possible to use the auto generated tactics on Windows as well. Also you can manually write CoqHammer tactic calls (that is use it as replacement for auto) on Windows.

• Note on Flocq: there is a new version 4.0 for coq-flocq which is not compatible with the previous 3.X versions. Since some packages are not yet compatible with Flocq 4.0, notably coq-compcert, the 2022.04 picks contain both, coq-flocq.4.0.0 and coq-flocq.3.4.3. Since one cannot install two version of one package, a new package called coq-flocq3 has been added which uses Flocq3 rather than Flocq as logical path. This way Flocq 3.X can be selected by using Flocq3 in the Require commands and Flocq 4.X can be selected by using Flocq in the Require commands. The package coq-compcert has been patched to require Flocq3. For convenience the proof automation packages used for float proofs, coq-gappa and coq-interval are also available in a Flocq 3.X and Flocq 4.X variant. The Flocq 4.X variants have the usual logical path, the 3.X variants use the logical paths IntervalFlocq3 and GappaFlocq3. The Flocq 3.X packages will be removed as soon as CompCert and VST are compatible with Flocq 4.0, but the opam packages will remain available and can be installed if needed.

• Note on gappa for flocq3: the flocq3 version of gappa requires a working sed in the path - which might be a problem on Windows since the installer does not install one.

• Note on QuickChick: QuickChick requires an OCaml compiler to run. The binary installers for Coq Platform do not provide OCaml, so QuickChick does not work with the binary installers for macOS, Windows and Snap. It is recommended to use the "compile from sources" method if you want to use QuickChick. An alternative method is to install OCaml by other means and have it in the PATH, but this method is not supported by the Coq Platform team. We plan to add an OCaml compiler to the binary installers in the next release.

Installers

Binary installers are provided for the 2022.04 pick of Coq 8.14 and 8.15 for macOS, Windows and Linux (snap). The macOS and Windows installers can be downloaded below. The snap package is available via the snapcraft.

2022.04.0

General information

See README for general information and installation of Coq Platform.

See Charter for the concept and goals of Coq Platform.

See CEP52 for the Coq and Coq Platform release cycle.

Major enhancements

The latest release version of Coq has been updated from 8.14.1 to 8.15.1 (see Coq 8.15 release notes)

QuickChick has been re-enabled on Windows, but only in "compile from sources" mode and not via the installer (this also applies to macOS and Snap).

Two packages have been added to the full level:

• coq-ott and ott, a domain specific language and too chain for formalizing programming languages and calculi
• coq-relation-algebra, a modular library for the algebra of relations with several high-level reflexive proof automation tactics

In addition two packages have been added to the extended level:

• coq-mathcomp-algebra-tactics, a library with field and ring tactics for mathcomp
• coq-extructures, a library for finite sets, maps and permutations which provide axiom free extensionality

Major changes

• coq-flocq has been updated to version 4.0.0, which is (slightly) incompatible with Flocq 3. Since coq-vst and coq-compcert have not yet switched to Flocq 4, Flocq 3 is included as a separate package - see the notes below for details.

Included Versions of Coq

Recommended Coq version

• Coq 8.15.1 with an extended and upgraded package collection

Compatibility Coq versions

The compatibility versions are intended to help porting packages from an older to the latest release. They can be installed in parallel with other versions of Coq (Coq Platform will create separate opam switches for each Coq version).

• Coq 8.14.1 with an updated package collection from Apr 2022 - this package pick is made to be as compatible as possible with the 8.15.1 package collection
• Coq 8.14.1 with the first package collection from Jan 2022
• Coq 8.13.2 with an updated package collection from January 2022 - this package pick is made to be as compatible as possible with the first 8.14.1 package collection
• Coq 8.13.2 with an updated package collection from September 2021
• Coq 8.13.2 with the original package collection from February 2021
• Coq 8.12.2 with the same package collection as the 8.12.2 Coq Platform release

Only the 8.14.1 and the 8.15.1 version are available as installers for macOS and Windows and only the 8.15.1 version as snap package. Other versions can be installed using the Coq Platform scripts.

Newly added / enabled packages:

• coq-quickchick is now available in "compile from sources" mode on all platforms, but not (yet) via installers
• coq-ott and ott, a domain specific language and too chain for formalizing programming languages and calculi
• coq-relation-algebra, a modular library for the algebra of relations with several high-level reflexive proof automation tactics
• coq-mathcomp-algebra-tactics, a library with field and ring tactics for mathcomp
• coq-extructures, a library for finite sets, maps and permutations which provide axiom free extensionality

See the package collection links in the Coq versions above for details on the included packages.

Removed packages:

(None)

Notes

• Notes on the macOS installer: This installer is only compatible with macOS 11.0 or higher. Because the application is signed but not "notarized", it won't open by default, unless you right-click the application in Finder and chose Open. Cf. #51 to learn more.

• Notes on Apple ARM silicon: Coq Platform has been tested by users on Apple silicon (M1), but we have no means to run CI tests on Apple silicon, so this not officially supported. We appreciate bug reports for Apple silicon, but we will ask you for help fixing them.

• Notes on CoqHammer: The proof generation component of CoqHammer is available on macOS and Linux only. The CoqHammer tactics, which reconstruct generated proofs, do work on Windows, though. Since the CoqHammer tactic running on macOS and Linux creates simple and fast Coq tactic call snippets which are intended to replace the slow generator tactics, it is possible to use the auto generated tactics on Windows as well. Also you can manually write CoqHammer tactic calls (that is use it as replacement for auto) on Windows.

• Note on Flocq: there is a new version 4.0 for coq-flocq which is not compatible with the previous 3.X versions. Since some packages are not yet compatible with Flocq 4.0, notably coq-compcert, the 2022.04 picks contain both, coq-flocq.4.0.0 and coq-flocq.3.4.3. Since one cannot install two version of one package, a new package called coq-flocq3 has been added which uses Flocq3 rather than Flocq as logical path. This way Flocq 3.X can be selected by using Flocq3 in the Require commands and Flocq 4.X can be selected by using Flocq in the Require commands. The package coq-compcert has been patched to require Flocq3. For convenience the proof automation packages used for float proofs, coq-gappa and coq-interval are also available in a Flocq 3.X and Flocq 4.X variant. The Flocq 4.X variants have the usual logical path, the 3.X variants use the logical paths IntervalFlocq3 and GappaFlocq3. The Flocq 3.X packages will be removed as soon as CompCert and VST are compatible with Flocq 4.0, but the opam packages will remain available and can be installed if needed.

• Note on QuickChick: QuickChick requires an OCaml compiler to run. The binary installers for Coq Platform do not provide OCaml, so QuickChick does not work with the binary installers for macOS, Windows and Snap. It is recommended to use the "compile from sources" method if you want to use QuickChick. An alternative method is to install OCaml by other means and have it in the PATH, but this method is not supported by the Coq Platform team. We plan to add an OCaml compiler to the binary installers in the next release.

Installers

Binary installers are provided for the 2022.04 pick of Coq 8.14 and 8.15 for macOS, Windows and Linux (snap). The macOS and Windows installers can be downloaded below. The snap package is available via the snapcraft.

2022.01.0

General information

See README for general information and installation of Coq Platform.

See Charter for the concept and goals of Coq Platform.

See CEP52 for the Coq and Coq Platform release cycle.

Major enhancements

An important newly added package, coq-hammer, provides the hammer tactic, which uses external ATPs (Automated Theorem Provers) to automatically create Coq proofs. Besides the plugin Coq Platform provides two automatically installed ATPs: E-Prover and Z3-TPTP. See the notes below on restrictions which (for the time being) apply to Windows users.

Another interesting new package, coq-coqprime-generator, provides the executables pocklington, o2v and firstprimes which automatically generate Coq proofs for the primality of (largish) prime numbers.

Included Versions of Coq

Recommended Coq version

• Coq 8.14.1 with an extended and upgraded package collection

Preview Coq versions

• Coq 8.15.0 with a preliminary (beta) package collection - all packages already support Coq 8.15.0, but some packages might still be updated.

Compatibility Coq versions

The compatibility versions are intended to help porting packages from an older to the latest release. They can be installed in parallel with other versions of Coq (Coq Platform will create separate opam switches for each Coq version).

• Coq 8.13.2 with an updated package collection from January 2022 - this package pick is made to be as compatible as possible with the 8.14.1 package pick
• Coq 8.13.2 with an updated package collection from September 2021
• Coq 8.13.2 with the original package collection from February 2021
• Coq 8.12.2 with the same package collection as the 8.12.2 Coq Platform release

Only the 8.14.1 and the 8.15.0 beta version are available as installers for macOS and Windows and only the 8.14.1 version as snap package. Other versions can be installed using the Coq Platform scripts.

Newly added packages:

• coq-hammer (not available on Windows)
• eprover ATP for coq-hammer (not available on Windows)
• z3_tptp ATP for coq-hammer (not available on Windows)
• coq-coqprime-generator

See the package collection links in the Coq versions above for details on the included packages.

Removed packages:

• coq-quickchick has been removed on Windows, because it does not work - we are working on getting it back with the 2022.03 release.

Notes

• Notes on the macOS installer: This installer is only compatible with macOS 10.13 or higher. Because the application is signed but not "notarized", on macOS 10.15 (Catalina) and 11.X (BigSur), it won't open by default, unless you right-click the application in Finder and chose Open. Cf. #51 to learn more.

• Notes on Apple ARM silicon: Coq Platform has been tested by users on Apple silicon (M1), but we have no means to run CI tests on Apple silicon, so this not officially supported. We appreciate bug reports for Apple silicon, but we will ask you for help fixing them.

• Note on the 8.15 version: This package pick contains Coq 8.15.0, but with a preliminary collection of packages. From a Coq Platform point of view, the Coq 8.15.0 variant is a beta release, so it is called 8.15~beta1. A Coq Platform release with a final package collection for Coq 8.15 is expected end of February 2022. The beta release is complete (all packages compile) and most versions have been confirmed by the package maintainers, so only minor changes are expected.

• Notes on CoqHammer: The proof generation component of CoqHammer is available on macOS and Linux only. The CoqHammer tactics, which reconstruct generated proofs, do work on Windows, though. Since the CoqHammer tactic running on macOS and Linux creates simple and fast Coq tactic call snippets which are intended to replace the slow generator tactics, it is possible to use the auto generated tactics on Windows as well. Also you can manually write CoqHammer tactic calls (that is use it as replacement for auto) on Windows.

Installers

Binary installers are provided for the 2022.01 pick of Coq 8.14 and 8.15 for macOS, Windows and Linux (snap). The macOS and Windows installers can be downloaded below. The snap package is available via the snapcraft.

Coq Platform 2021.09.0

General information

See README for general information and installation of Coq Platform.

See Charter for the concept and goals of Coq Platform.

See CEP52 for the Coq and Coq Platform release cycle.

Major enhancements

The 2021.09.0 release of the Coq Platform has two major enhancements:

• support for installing several versions of Coq (also in parallel)
• substantially extended collection of Coq packages

Included Versions of Coq

Recommended Coq version

• Coq 8.13.2 with the extended and upgraded package collection

Preview Coq versions

• Coq 8.14.0 with a preliminary (beta) package collection - not all packages support Coq 8.14 yet
• Coq 8.14.0 with a not yet released extension: an interactive Ltac-Debugger for CoqIDE

Compatibility Coq versions

The compatibility versions are intended to help porting packages from an older to the latest release. They can be installed in parallel with other versions of Coq (Coq Platform will create separate opam switches for each Coq version).

• Coq 8.13.2 with the original package collection from February 2021
• Coq 8.12.2 with the same package collection as the 8.12.2 Coq Platform release

Only the extended 8.13.2 version and the 8.14.0 beta version are available as installers for macOS and Windows and only the extended 8.13.2 version as snap package. Other versions can be installed using the Coq Platform scripts.

Newly added packages:

• coq-coqeal
• coq-coqprime
• coq-corn
• coq-deriving
• coq-dpdgraph
• coq-hammer-tactics
• coq-hott
• coq-iris
• coq-iris-heap-lang
• coq-libhyps
• coq-math-classes
• coq-mathcomp-analysis
• coq-mathcomp-multinomials
• coq-mathcomp-zify
• coq-paramcoq
• coq-record-update
• coq-reduction-effects
• coq-reglang
• coq-serapi
• coq-stdpp
• coq-unimath

See the package collection links in the Coq versions above for details on the included packages.

Notes

• Notes regarding the macOS installer: This installer is only compatible with macOS 10.13 or higher. Because the application is signed but not "notarized", on macOS 10.15 (Catalina) and 11.X (BigSur), it won't open by default, unless you right-click the application in Finder and chose Open. Cf. #51 to learn more.

• Notes on Apple ARM silicon: Coq Platform currently does not support Apple ARM silicon (M1) - it should be easy to fix but we currently have no access to such HW and also cannot test it in CI. See (#168) and Github support. Please ping us via the linked ticket if you have Apple silicon and want to have an online debug session with us.

• Note on the 8.14 version: Coq Platform 2021.09.0 includes Coq 8.14.0, but with a preliminary collection of packages. From a Coq Platform point of view, the Coq 8.14 variant is a beta release, so it is called 2021.09.0~8.14+beta2. A Coq Platform release with a final package collection for Coq 8.14 is expected end of November 2021.

Coq Platform 2021.02.2

This release contains the same version of Coq and Coq packages as the 2021.02.1 release. A new release was required because of incompatible changes in opam and Cygwin. The list of changes is:

• support for opam 2.1.0 (which integrates the opam system dependency manager depext - this needed a few adjustments)
• fix issues with Cygwin binutils
• various minor fixes for the Snap package (support gappa, clightgen, ...)
• various minor fixes to the Windows installer (add icon for CoqIDE, ...)
• minor cleanup and improvements of the Coq Platform scripts

See the ReadMe for details on the names and versions of the included packages.

There are two ways to install the Coq Platform:

• Beginners are advised to rely on the binary packages. There are a DMG installer package for macOS, 32 and 64 bit Windows installers (see asset list below) and a Snap installer (see README_Linux for details).

• Experienced users are advised to install from source using the opam based interactive platform scripts.

See the following OS-specific documentation for details:

• macOS: see README_macOS.
• Windows: see README_Windows
• Linux: see README_Linux.

Notes regarding the macOS installer: This installer is only compatible with macOS 10.13 or higher. Because the application is signed but not "notarized", on macOS 10.15 (Catalina) and 11.X (BigSur), it won't open by default, unless you right-click the application in Finder and chose Open. Cf. #51 to learn more.

Coq Platform 2021.02.1

This release of the Coq Platform contains Coq 8.13.2 and the following updates and additions:

• A DMG installer package for macOS (new)
• The Homotopy Type Theory library coq-hott version 8.13 (new)
• The Verified Software Toolchain coq-vst version 2.7.1 (update)

See the ReadMe for details on the names and versions of the included packages.

There are two ways to install the Coq Platform:

• Beginners are advised to rely on the binary packages. There are a DMG installer package for macOS, 32 and 64 bit Windows installers (see asset list below) and a Snap installer (see README_Linux for details).

• Experienced users are advised to install from source using the opam based interactive platform scripts.

See the following OS-specific documentation for details:

• macOS: see README_macOS.
• Windows: see README_Windows
• Linux: see README_Linux.