Coq Versions Save

See the changelog for an overview of the new features and changes.

Mostly CoqIDE fixes.

See the changelog for detailed changes.

Main fixes:

• inconsistency with module subtyping and inductive types (https://github.com/coq/coq/issues/15838)
• CoqIDE slowdown on large files
• missing .vok file creation
• cbn regression (https://github.com/coq/coq/issues/15567)
• usability of schemes with elim foo using scheme with (P0 := ...) (the P0 name was not accessible in 8.15.0) (https://github.com/coq/coq/issues/15420)

See the changelog for detailed changes.

See the changelog for an overview of the new features and changes.

See the changelog for an overview of the bug fixes.

See https://coq.github.io/doc/v8.15/refman/changes.html#changes-in-8-15-0

The 8.15 release will not have any more changes other than bug fixes with low compatibility impact.

See the changelog for an overview of the new features and changes.

Hotfix:

• Fix crash when using vm_compute on an irreducible PArray.set
• Fix crash when loading .vo files containing a vm_compute normalized primitive array
• Fix Ltac2.Array.init computational complexity

Packages:

• binary packages are provided by the Coq Platform version 2021.02.1, see the platform release page

Hotfix:

• Fix arities of VM opcodes for some floating-point operations that could cause memory corruption

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), it won't open by default, unless you right-click and chose "Open". Cf. https://github.com/coq/platform/issues/51 to learn more.

Notes regarding the Windows installer: ~The "VST" component of the installer is currently empty. We are working on a fix.~ Update: installers are now complete.

Highlights:

• Introduction of primitive persistent arrays in the core language, implemented using imperative persistent arrays.
• Introduction of definitional proof irrelevance for the equality type defined in the SProp sort.
• Many improvements to the handling of notations, including number notations, recursive notations and notations with bindings. A new algorithm chooses the most precise notation available to print an expression, which might introduce changes in printing behavior.

See the changelog for an overview of the new features and changes.

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), it won't open by default, unless you right-click and chose "Open". Cf. https://github.com/coq/platform/issues/51 to learn more.

Update: The OSX bundle was regenerated in order to include the missing file libgmp