Skip to content

2024.10.0 with latest pick Coq 8.19~2024.10

Latest
Latest
Compare
Choose a tag to compare
@MSoegtropIMC MSoegtropIMC released this 28 Oct 13:30
· 8 commits to main since this release
2024.10.0
483a341
This commit was created on GitHub.com and signed with GitHub’s verified signature.
GPG key ID: B5690EEEBB952194
Learn about vigilant mode.

Recommended binary installers

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

  • The MacOS installer is now not only signed, but also notarized. This means it can be opened on latest MacOS without work-arounds. You still have to confirm that you want to run an application downloaded from the internet.
  • There are two major technical enhancements on Windows:
    • Support for arbitrary path length has been enabled by compiling all executables with a corresponding manifest. In addition this needs to globally enabled in the registry.
      The "build from sources" scripts check if this is enabled and if not ask the user to enable it. For running Coq from an installer arbitrary path length support is not required.
    • Ocamlc is patched to allow 64MB stack size - this way latest fiat-crypto can be build.
      Note that other applications, notably coqc, are not patched.
      The program to do the patches is available in the platform and can be used for other executables as well if needed.
      Now all Coq Platform packages are available on Windows, except coq-hammer (which makes heavy use of Unix fork)

No new packages have been added - this will be done in a soon to follow minor release.

Included Versions of Coq

Recommended Coq version

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.18.0 with the first package collection from November 2023
  • 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 Coq 8.19.2 based package collections are available as installers for macOS and Windows. Other versions can be installed using the Coq Platform scripts or the binary installers from previous Platform releases.

Notes

  • Notes on the macOS installer: The command file to open a Coq Platform shell "coq-shell8.192024.10.command" is not yet signed. You can still open it by CMD+click / right click on it and open. This is required only once.

  • Notes on the macOS Intel installer: There are some issues with the Intel installer - it will be provided later.

  • 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 and Windows. 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 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 Coq 8.19.2. The Installer for MacOS Apple silicon and the Windows installer can be downloaded below. The MacOS installer for Intel silicon will be available soon.

Assets 7
Loading