You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
Gives a result like (stripped to fit in GitHub's max length for issues):
{
"data": {
"repository": {
"releases": {
"nodes": [
{
"tag": {
"name": "V8.20.0"
},
"name": "Coq 8.20.0",
"description": "See the [changelog](https://coq.github.io/doc/v8.20/refman/changes.html#changes-in-8-20-0) for an overview of the new features and changes.",
"url": "https://github.com/coq/coq/releases/tag/V8.20.0",
"isDraft": false,
"publishedAt": "2024-09-04T11:32:58Z",
"isPrerelease": false,
"releaseAssets": {
"nodes": [
{
"name": "coq-8.20.0.tar.gz",
"downloadUrl": "https://github.com/coq/coq/releases/download/V8.20.0/coq-8.20.0.tar.gz"
},
{
"name": "coq-8.20.0-reference-manual.pdf",
"downloadUrl": "https://github.com/coq/coq/releases/download/V8.20.0/coq-8.20.0-reference-manual.pdf"
}
]
}
},
{
"tag": {
"name": "V8.20+rc1"
},
"name": "Coq 8.20+rc1",
"description": "See the [changelog](https://coq.github.io/doc/v8.20/refman/changes.html#changes-in-8-20-0) for an overview of the new features and changes.",
"url": "https://github.com/coq/coq/releases/tag/V8.20%2Brc1",
"isDraft": false,
"publishedAt": "2024-06-27T12:56:14Z",
"isPrerelease": false,
"releaseAssets": {
"nodes": [
{
"name": "coq-8.20-rc1.tar.gz",
"downloadUrl": "https://github.com/coq/coq/releases/download/V8.20%2Brc1/coq-8.20-rc1.tar.gz"
},
{
"name": "coq-8.20+rc1-reference-manual.pdf",
"downloadUrl": "https://github.com/coq/coq/releases/download/V8.20%2Brc1/coq-8.20%2Brc1-reference-manual.pdf"
}
]
}
},
{
"tag": {
"name": "V8.19.2"
},
"name": "Coq 8.19.2",
"description": "See the [changelog](https://coq.github.io/doc/v8.19/refman/changes.html#changes-in-8-19-2) (or changelog section in the attached manual) for an overview of the new bug fixes and changes.",
"url": "https://github.com/coq/coq/releases/tag/V8.19.2",
"isDraft": false,
"publishedAt": "2024-06-10T11:30:17Z",
"isPrerelease": false,
"releaseAssets": {
"nodes": [
{
"name": "coq-8.19.2-reference-manual.pdf",
"downloadUrl": "https://github.com/coq/coq/releases/download/V8.19.2/coq-8.19.2-reference-manual.pdf"
},
{
"name": "coq-8.19.2.tar.gz",
"downloadUrl": "https://github.com/coq/coq/releases/download/V8.19.2/coq-8.19.2.tar.gz"
}
]
}
},
{
"tag": {
"name": "V8.19.1"
},
"name": "Coq 8.19.1",
"description": "See the [changelog](https://coq.github.io/doc/v8.19/refman/changes.html#changes-in-8-19-1) for an overview of the new features and changes.",
"url": "https://github.com/coq/coq/releases/tag/V8.19.1",
"isDraft": false,
"publishedAt": "2024-03-04T13:01:12Z",
"isPrerelease": false,
"releaseAssets": {
"nodes": [
{
"name": "coq-8.19.1-reference-manual.pdf",
"downloadUrl": "https://github.com/coq/coq/releases/download/V8.19.1/coq-8.19.1-reference-manual.pdf"
},
{
"name": "coq-8.19.1.tar.gz",
"downloadUrl": "https://github.com/coq/coq/releases/download/V8.19.1/coq-8.19.1.tar.gz"
}
]
}
},
{
"tag": {
"name": "V8.19.0"
},
"name": "Coq 8.19.0",
"description": "See the [changelog](https://coq.github.io/doc/v8.19/refman/changes.html#changes-in-8-19-0) for an overview of the new features and changes.",
"url": "https://github.com/coq/coq/releases/tag/V8.19.0",
"isDraft": false,
"publishedAt": "2024-01-24T12:49:50Z",
"isPrerelease": false,
"releaseAssets": {
"nodes": [
{
"name": "coq-8.19.0-reference-manual.pdf",
"downloadUrl": "https://github.com/coq/coq/releases/download/V8.19.0/coq-8.19.0-reference-manual.pdf"
},
{
"name": "coq-8.19.0.tar.gz",
"downloadUrl": "https://github.com/coq/coq/releases/download/V8.19.0/coq-8.19.0.tar.gz"
}
]
}
},
{
"tag": {
"name": "V8.19+rc1"
},
"name": "Coq 8.19+rc1",
"description": "See the [changelog](https://coq.github.io/doc/v8.19/refman/changes.html#changes-in-8-19-0) for an overview of the new features and changes.",
"url": "https://github.com/coq/coq/releases/tag/V8.19%2Brc1",
"isDraft": false,
"publishedAt": "2023-12-18T16:31:49Z",
"isPrerelease": true,
"releaseAssets": {
"nodes": [
{
"name": "coq-8.19.0-reference-manual.pdf",
"downloadUrl": "https://github.com/coq/coq/releases/download/V8.19%2Brc1/coq-8.19.0-reference-manual.pdf"
},
{
"name": "coq-8.19-rc1.tar.gz",
"downloadUrl": "https://github.com/coq/coq/releases/download/V8.19%2Brc1/coq-8.19-rc1.tar.gz"
}
]
}
},
{
"tag": {
"name": "V8.18.0"
},
"name": "Coq 8.18.0",
"description": "See the [changelog](https://coq.github.io/doc/v8.18/refman/changes.html#changes-in-8-18-0) for an overview of the new features and changes.",
"url": "https://github.com/coq/coq/releases/tag/V8.18.0",
"isDraft": false,
"publishedAt": "2023-09-08T10:32:30Z",
"isPrerelease": false,
"releaseAssets": {
"nodes": [
{
"name": "coq-8.18.0-reference-manual.pdf",
"downloadUrl": "https://github.com/coq/coq/releases/download/V8.18.0/coq-8.18.0-reference-manual.pdf"
},
{
"name": "coq-8.18.0.tar.gz",
"downloadUrl": "https://github.com/coq/coq/releases/download/V8.18.0/coq-8.18.0.tar.gz"
}
]
}
},
{
"tag": {
"name": "V8.18+rc1"
},
"name": "Coq 8.18+rc1",
"description": "See the [changelog](https://coq.github.io/doc/v8.18/refman/changes.html) for an overview of the new features and changes.",
"url": "https://github.com/coq/coq/releases/tag/V8.18%2Brc1",
"isDraft": false,
"publishedAt": "2023-08-03T11:52:34Z",
"isPrerelease": true,
"releaseAssets": {
"nodes": [
{
"name": "coq-8.18+rc1.tar.gz",
"downloadUrl": "https://github.com/coq/coq/releases/download/V8.18%2Brc1/coq-8.18%2Brc1.tar.gz"
},
{
"name": "coq-8.18+rc1-reference-manual.pdf",
"downloadUrl": "https://github.com/coq/coq/releases/download/V8.18%2Brc1/coq-8.18%2Brc1-reference-manual.pdf"
}
]
}
},
{
"tag": {
"name": "V8.17.1"
},
"name": "Coq 8.17.1",
"description": "See the [changelog](https://coq.github.io/doc/v8.17/refman/changes.html#changes-in-8-17-1) for an overview of the new features and changes.",
"url": "https://github.com/coq/coq/releases/tag/V8.17.1",
"isDraft": false,
"publishedAt": "2023-06-27T09:17:52Z",
"isPrerelease": false,
"releaseAssets": {
"nodes": [
{
"name": "coq-8.17.1-reference-manual.pdf",
"downloadUrl": "https://github.com/coq/coq/releases/download/V8.17.1/coq-8.17.1-reference-manual.pdf"
}
]
}
},
{
"tag": {
"name": "V8.17.0"
},
"name": "Coq 8.17.0",
"description": "See the [changelog](https://coq.github.io/doc/v8.17/refman/changes.html#changes-in-8-17-0) for an overview of the new features and changes.",
"url": "https://github.com/coq/coq/releases/tag/V8.17.0",
"isDraft": false,
"publishedAt": "2023-03-27T06:40:40Z",
"isPrerelease": false,
"releaseAssets": {
"nodes": [
{
"name": "coq-8.17.0-reference-manual.pdf",
"downloadUrl": "https://github.com/coq/coq/releases/download/V8.17.0/coq-8.17.0-reference-manual.pdf"
}
]
}
},
{
"tag": {
"name": "V8.17+rc1"
},
"name": "Coq 8.17+rc1",
"description": "See the [changelog](https://coq.github.io/doc/v8.17/refman/changes.html#changes-in-8-17-0) for an overview of the new features and changes.",
"url": "https://github.com/coq/coq/releases/tag/V8.17%2Brc1",
"isDraft": false,
"publishedAt": "2023-01-16T15:41:43Z",
"isPrerelease": true,
"releaseAssets": {
"nodes": [
{
"name": "coq-8.17.0-reference-manual.pdf",
"downloadUrl": "https://github.com/coq/coq/releases/download/V8.17%2Brc1/coq-8.17.0-reference-manual.pdf"
}
]
}
},
{
"tag": {
"name": "V8.16.1"
},
"name": "Coq 8.16.1",
"description": "See the [changelog](https://coq.inria.fr/distrib/V8.16.1/refman/changes.html) for an overview of the new features and changes.",
"url": "https://github.com/coq/coq/releases/tag/V8.16.1",
"isDraft": false,
"publishedAt": "2022-11-25T14:47:27Z",
"isPrerelease": false,
"releaseAssets": {
"nodes": [
{
"name": "coq-8.16.1-reference-manual.pdf",
"downloadUrl": "https://github.com/coq/coq/releases/download/V8.16.1/coq-8.16.1-reference-manual.pdf"
}
]
}
},
{
"tag": {
"name": "V8.16.0"
},
"name": "Coq 8.16.0",
"description": "See the [changelog](https://coq.inria.fr/distrib/V8.16.0/refman/changes.html) for an overview of the new features and changes.",
"url": "https://github.com/coq/coq/releases/tag/V8.16.0",
"isDraft": false,
"publishedAt": "2022-09-05T11:57:41Z",
"isPrerelease": false,
"releaseAssets": {
"nodes": [
{
"name": "coq-8.16.0-reference-manual.pdf",
"downloadUrl": "https://github.com/coq/coq/releases/download/V8.16.0/coq-8.16.0-reference-manual.pdf"
}
]
}
},
{
"tag": {
"name": "V8.16+rc1"
},
"name": "Coq 8.16+rc1",
"description": "See the [changelog](https://coq.github.io/doc/v8.16/refman/changes.html#changes-in-8-16-0) for an overview of the new features and changes.",
"url": "https://github.com/coq/coq/releases/tag/V8.16%2Brc1",
"isDraft": false,
"publishedAt": "2022-08-08T14:17:12Z",
"isPrerelease": true,
"releaseAssets": {
"nodes": [
{
"name": "coq-8.16+rc1-reference-manual.pdf",
"downloadUrl": "https://github.com/coq/coq/releases/download/V8.16%2Brc1/coq-8.16%2Brc1-reference-manual.pdf"
}
]
}
},
{
"tag": {
"name": "V8.15.2"
},
"name": "Coq 8.15.2",
"description": "Mostly CoqIDE fixes.\r\n\r\nSee the [changelog](https://coq.github.io/doc/v8.15/refman/changes.html#changes-in-8-15-2) for detailed changes.",
"url": "https://github.com/coq/coq/releases/tag/V8.15.2",
"isDraft": false,
"publishedAt": "2022-05-31T11:57:12Z",
"isPrerelease": false,
"releaseAssets": {
"nodes": [
{
"name": "coq-8.15.2-reference-manual.pdf",
"downloadUrl": "https://github.com/coq/coq/releases/download/V8.15.2/coq-8.15.2-reference-manual.pdf"
}
]
}
},
{
"tag": {
"name": "V8.15.1"
},
"name": "Coq 8.15.1",
"description": "Main fixes:\r\n- inconsistency with module subtyping and inductive types (https://github.com/coq/coq/issues/15838)\r\n- CoqIDE slowdown on large files \r\n- missing `.vok` file creation\r\n- cbn regression (https://github.com/coq/coq/issues/15567)\r\n- 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) \r\n\r\nSee the [changelog](https://coq.github.io/doc/v8.15/refman/changes.html#changes-in-8-15-1) for detailed changes.",
"url": "https://github.com/coq/coq/releases/tag/V8.15.1",
"isDraft": false,
"publishedAt": "2022-03-22T16:36:15Z",
"isPrerelease": false,
"releaseAssets": {
"nodes": [
{
"name": "coq-8.15.1-reference-manual.pdf",
"downloadUrl": "https://github.com/coq/coq/releases/download/V8.15.1/coq-8.15.1-reference-manual.pdf"
}
]
}
},
{
"tag": {
"name": "V8.15.0"
},
"name": "Coq 8.15.0",
"description": "See the [changelog](https://coq.github.io/doc/v8.15/refman/changes.html#version-8-15) for an overview of the new features and changes.",
"url": "https://github.com/coq/coq/releases/tag/V8.15.0",
"isDraft": false,
"publishedAt": "2022-01-13T16:28:58Z",
"isPrerelease": false,
"releaseAssets": {
"nodes": [
{
"name": "coq-8.15.0-reference-manual.pdf",
"downloadUrl": "https://github.com/coq/coq/releases/download/V8.15.0/coq-8.15.0-reference-manual.pdf"
}
]
}
},
{
"tag": {
"name": "V8.15+rc1"
},
"name": "Coq 8.15+rc1",
"description": "See https://coq.github.io/doc/v8.15/refman/changes.html#changes-in-8-15-0\r\n\r\nThe 8.15 release will not have any more changes other than bug fixes with low compatibility impact.",
"url": "https://github.com/coq/coq/releases/tag/V8.15%2Brc1",
"isDraft": false,
"publishedAt": "2021-12-07T15:16:26Z",
"isPrerelease": true,
"releaseAssets": {
"nodes": [
{
"name": "coq-8.15+rc1-reference-manual.pdf",
"downloadUrl": "https://github.com/coq/coq/releases/download/V8.15%2Brc1/coq-8.15%2Brc1-reference-manual.pdf"
}
]
}
},
{
"tag": {
"name": "V8.14.1"
},
"name": "Coq 8.14.1",
"description": "See the [changelog](https://coq.github.io/doc/v8.14/refman/changes.html#changes-in-8-14-1) for an overview of the bug fixes.",
"url": "https://github.com/coq/coq/releases/tag/V8.14.1",
"isDraft": false,
"publishedAt": "2021-12-07T15:54:23Z",
"isPrerelease": false,
"releaseAssets": {
"nodes": [
{
"name": "coq-8.14.1-reference-manual.pdf",
"downloadUrl": "https://github.com/coq/coq/releases/download/V8.14.1/coq-8.14.1-reference-manual.pdf"
}
]
}
},
{
"tag": {
"name": "V8.14.0"
},
"name": "Coq 8.14.0",
"description": "See the [changelog](https://coq.github.io/doc/v8.14/refman/changes.html#version-8-14) for an overview of the new features and changes.",
"url": "https://github.com/coq/coq/releases/tag/V8.14.0",
"isDraft": false,
"publishedAt": "2021-10-14T13:03:18Z",
"isPrerelease": false,
"releaseAssets": {
"nodes": [
{
"name": "coq-8.14.0-reference-manual.pdf",
"downloadUrl": "https://github.com/coq/coq/releases/download/V8.14.0/coq-8.14.0-reference-manual.pdf"
}
]
}
},
{
"tag": {
"name": "V8.13.2"
},
"name": "Coq 8.13.2",
"description": "Hotfix:\r\n- Fix crash when using `vm_compute` on an irreducible `PArray.set`\r\n- Fix crash when loading `.vo` files containing a `vm_compute` normalized primitive array\r\n- Fix `Ltac2.Array.init` computational complexity\r\n\r\nPackages:\r\n- binary packages are provided by the Coq Platform version 2021.02.1, see the platform [release page](https://github.com/coq/platform/releases)",
"url": "https://github.com/coq/coq/releases/tag/V8.13.2",
"isDraft": false,
"publishedAt": "2021-04-12T08:10:47Z",
"isPrerelease": false,
"releaseAssets": {
"nodes": [
{
"name": "coq-8.13.2-reference-manual.pdf",
"downloadUrl": "https://github.com/coq/coq/releases/download/V8.13.2/coq-8.13.2-reference-manual.pdf"
}
]
}
},
{
"tag": {
"name": "V8.13.1"
},
"name": "Coq 8.13.1",
"description": "Hotfix:\r\n- Fix arities of VM opcodes for some floating-point operations that could cause memory corruption\r\n\r\n__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.\r\n\r\n__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.",
"url": "https://github.com/coq/coq/releases/tag/V8.13.1",
"isDraft": false,
"publishedAt": "2021-02-22T13:32:09Z",
"isPrerelease": false,
"releaseAssets": {
"nodes": [
{
"name": "coq-8.13.1-installer-macos.dmg",
"downloadUrl": "https://github.com/coq/coq/releases/download/V8.13.1/coq-8.13.1-installer-macos.dmg"
},
{
"name": "coq-8.13.1-reference-manual.pdf",
"downloadUrl": "https://github.com/coq/coq/releases/download/V8.13.1/coq-8.13.1-reference-manual.pdf"
},
{
"name": "coq-8.13.1-installer-windows-i686.exe",
"downloadUrl": "https://github.com/coq/coq/releases/download/V8.13.1/coq-8.13.1-installer-windows-i686.exe"
},
{
"name": "coq-8.13.1-installer-windows-x86_64.exe",
"downloadUrl": "https://github.com/coq/coq/releases/download/V8.13.1/coq-8.13.1-installer-windows-x86_64.exe"
}
]
}
},
{
"tag": {
"name": "V8.13.0"
},
"name": "Coq 8.13.0",
"description": "Highlights:\r\n- Introduction of primitive persistent arrays in the core language, implemented using imperative persistent arrays.\r\n- Introduction of definitional proof irrelevance for the equality type defined in the SProp sort.\r\n- 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.\r\n\r\nSee the [changelog](https://coq.github.io/doc/v8.13/refman/changes.html#version-8-13) for an overview of the new features and changes.\r\n\r\n__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.\r\n\r\n__Update__: The OSX bundle was regenerated in order to include the missing file libgmp",
"url": "https://github.com/coq/coq/releases/tag/V8.13.0",
"isDraft": false,
"publishedAt": "2021-01-07T09:35:45Z",
"isPrerelease": false,
"releaseAssets": {
"nodes": [
{
"name": "coq-8.13.0-installer-windows-i686.exe",
"downloadUrl": "https://github.com/coq/coq/releases/download/V8.13.0/coq-8.13.0-installer-windows-i686.exe"
},
{
"name": "coq-8.13.0-installer-windows-x86_64.exe",
"downloadUrl": "https://github.com/coq/coq/releases/download/V8.13.0/coq-8.13.0-installer-windows-x86_64.exe"
},
{
"name": "coq-8.13.0-installer-macos.dmg",
"downloadUrl": "https://github.com/coq/coq/releases/download/V8.13.0/coq-8.13.0-installer-macos.dmg"
},
{
"name": "coq-8.13.0-reference-manual.pdf",
"downloadUrl": "https://github.com/coq/coq/releases/download/V8.13.0/coq-8.13.0-reference-manual.pdf"
}
]
}
},
{
"tag": {
"name": "V8.12.2"
},
"name": "Coq 8.12.2",
"description": "This release fixes two impacting 8.12 regressions (in notations and the implicit argument inference of the `exists` tactic). See [changelog](https://coq.inria.fr/distrib/V8.12.2/refman/changes.html#changes-in-8-12-2).\r\n\r\n**New:** a 64-bit Windows [Coq platform](https://github.com/coq/platform) installer is now available. A 32-bit Windows installer should eventually become available.",
"url": "https://github.com/coq/coq/releases/tag/V8.12.2",
"isDraft": false,
"publishedAt": "2020-12-11T10:34:09Z",
"isPrerelease": false,
"releaseAssets": {
"nodes": [
{
"name": "coq-8.12.2-reference-manual.pdf",
"downloadUrl": "https://github.com/coq/coq/releases/download/V8.12.2/coq-8.12.2-reference-manual.pdf"
},
{
"name": "coq-8.12.2-installer-macos.dmg",
"downloadUrl": "https://github.com/coq/coq/releases/download/V8.12.2/coq-8.12.2-installer-macos.dmg"
},
{
"name": "coq-8.12.2-installer-windows-x86_64.exe",
"downloadUrl": "https://github.com/coq/coq/releases/download/V8.12.2/coq-8.12.2-installer-windows-x86_64.exe"
}
]
}
},
{
"tag": {
"name": "V8.13+beta1"
},
"name": "Coq 8.13+beta1",
"description": "We encourage our users to test this beta release, in particular:\r\n\r\n- The windows installer is now based on the Coq platform: This\r\n greatly simplifies its build process and makes it easy to add \r\n more packages. At the same time this new installer was only\r\n tested by two people, so if you use Windows please give us\r\n feedback on any problem you may encounter.\r\n\r\n- The notation system received many fixes and improvements, in\r\n particular the way notations are selected for printing changed:\r\n Coq now prefers notations which match a larger part of the term to\r\n abbreviate, and takes into account the order in which notations are \r\n imported in the current scope only in a second instance.\r\n The new rules were designed together with power users, and tested\r\n by some of them, but our automatic testing infrastructure for \r\n regressions in notation printing is still weak. If your Coq library\r\n makes heavy use of notations, please give us feedback on any \r\n regression.\r\n\r\nSee the [changelog](https://coq.github.io/doc/v8.13/refman/changes.html#version-8-13) for the complete list of changes.",
"url": "https://github.com/coq/coq/releases/tag/V8.13%2Bbeta1",
"isDraft": false,
"publishedAt": "2020-12-07T14:52:44Z",
"isPrerelease": true,
"releaseAssets": {
"nodes": [
{
"name": "coq-8.13+beta1-installer-macos.dmg",
"downloadUrl": "https://github.com/coq/coq/releases/download/V8.13%2Bbeta1/coq-8.13%2Bbeta1-installer-macos.dmg"
},
{
"name": "coq-8.13+beta1-installer-windows-x86_64.exe",
"downloadUrl": "https://github.com/coq/coq/releases/download/V8.13%2Bbeta1/coq-8.13%2Bbeta1-installer-windows-x86_64.exe"
},
{
"name": "coq-8.13+beta1-reference-manual.pdf",
"downloadUrl": "https://github.com/coq/coq/releases/download/V8.13%2Bbeta1/coq-8.13%2Bbeta1-reference-manual.pdf"
}
]
}
},
{
"tag": {
"name": "V8.12.1"
},
"name": "Coq 8.12.1",
"description": "This release contains numerous bug fixes and documentation improvements. Some bug fix highlights:\r\n\r\n- Polymorphic side-effects inside monomorphic definitions were incorrectly handled as not inlined. This allowed deriving an inconsistency (#13330).\r\n- Regression in error reporting after SSReflect's `case` tactic. A generic error message \"Could not fill dependent hole in apply\" was reported for any error following `case` or `elim` (#12837).\r\n- Several bugs with `Search` (#13298, #13349).\r\n- The `details` environment introduced in coqdoc in Coq 8.12 can now be used as advertised in the reference manual (#12772).\r\n- View menu \"Display parentheses\" introduced in CoqIDE in Coq 8.12 now works correctly (#12793).\r\n\r\nSee the [changelog](https://coq.inria.fr/refman/changes.html#changes-in-8-12-1) for details and a more complete list.\r\n\r\n**New**: a macOS installer is now available.",
"url": "https://github.com/coq/coq/releases/tag/V8.12.1",
"isDraft": false,
"publishedAt": "2020-11-16T13:39:19Z",
"isPrerelease": false,
"releaseAssets": {
"nodes": [
{
"name": "coq-8.12.1-reference-manual.pdf",
"downloadUrl": "https://github.com/coq/coq/releases/download/V8.12.1/coq-8.12.1-reference-manual.pdf"
},
{
"name": "coq-8.12.1-installer-windows-i686.exe",
"downloadUrl": "https://github.com/coq/coq/releases/download/V8.12.1/coq-8.12.1-installer-windows-i686.exe"
},
{
"name": "coq-8.12.1-installer-windows-x86_64.exe",
"downloadUrl": "https://github.com/coq/coq/releases/download/V8.12.1/coq-8.12.1-installer-windows-x86_64.exe"
},
{
"name": "coq-8.12.1-installer-macos.dmg",
"downloadUrl": "https://github.com/coq/coq/releases/download/V8.12.1/coq-8.12.1-installer-macos.dmg"
}
]
}
},
{
"tag": {
"name": "V8.12.0"
},
"name": "Coq 8.12.0",
"description": "Some highlights from this release are:\r\n- a new binder notation for non-maximal implicit arguments;\r\n- an improved `Search` command which accepts more complex queries;\r\n- many additions to the standard library;\r\n- a restructured reference manual;\r\n- the deprecation of the `omega` tactic in favor the `lia` tactic.\r\n\r\nPlease see [the changelog](https://coq.github.io/doc/v8.12/refman/changes.html#version-8-12) to learn more about this release.\r\n\r\n### Notes regarding the macOS installer\r\n\r\nThis 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.",
"url": "https://github.com/coq/coq/releases/tag/V8.12.0",
"isDraft": false,
"publishedAt": "2020-07-27T14:45:38Z",
"isPrerelease": false,
"releaseAssets": {
"nodes": [
{
"name": "coq-8.12.0-installer-windows-i686.exe",
"downloadUrl": "https://github.com/coq/coq/releases/download/V8.12.0/coq-8.12.0-installer-windows-i686.exe"
},
{
"name": "coq-8.12.0-reference-manual.pdf",
"downloadUrl": "https://github.com/coq/coq/releases/download/V8.12.0/coq-8.12.0-reference-manual.pdf"
},
{
"name": "coq-8.12.0-installer-windows-x86_64.exe",
"downloadUrl": "https://github.com/coq/coq/releases/download/V8.12.0/coq-8.12.0-installer-windows-x86_64.exe"
},
{
"name": "coq-8.12.0-installer-macos.dmg",
"downloadUrl": "https://github.com/coq/coq/releases/download/V8.12.0/coq-8.12.0-installer-macos.dmg"
}
]
}
},
{
"tag": {
"name": "V8.12+beta1"
},
"name": "Coq 8.12+beta1",
"description": "<p>We are happy to announce the first beta release of Coq 8.12.\r\n\r\n<p>This new version integrates many usability improvements, in\r\nparticular to notations, scopes and implicit arguments, along with\r\nmany bug fixes and major improvements to the reference manual. See the\r\n<a\r\nhref=\"https://coq.github.io/doc/v8.12/refman/changes.html#version-8-12\">changelog</a>\r\nfor details.\r\n\r\n<p>As usual, we are looking for <a\r\nhref=\"https://github.com/coq/coq/issues\">feedback from beta\r\ntesters</a>. In addition, we are looking for beta readers of the <a\r\nhref=\"https://coq.github.io/doc/v8.12/refman/\">updated reference\r\nmanual</a>.\r\n\r\n<p>The 8.12 improvements to the reference manual are the start of an\r\neffort to improve Coq documentation. We believe the documentation\r\nneeds considerable work to better serve the needs of the Coq\r\ncommunity. Better documentation will encourage more people to learn,\r\nteach and use Coq. We need your help for this. We're looking for\r\nvolunteers who will help rewrite or add new material (such as better\r\nexplanations and new examples) to the new pages. Writers do not have\r\nto be experts on their topic: we can pair writers with experts that\r\ncan answer questions and provide examples. Indeed, it's a great way to\r\nlearn more about Coq. We'd also appreciate specific feedback, perhaps\r\ndetailed, on what needs to be improved, what's missing and what things\r\nto improve first. If you are willing to help, please see the <a\r\nhref=\"https://github.com/coq/coq/wiki/Refman-improvements-in-8.12-and-beyond\">dedicated\r\nwiki page</a> to learn more.",
"url": "https://github.com/coq/coq/releases/tag/V8.12%2Bbeta1",
"isDraft": false,
"publishedAt": "2020-06-18T15:25:14Z",
"isPrerelease": true,
"releaseAssets": {
"nodes": [
{
"name": "coq-8.12+beta1-reference-manual.pdf",
"downloadUrl": "https://github.com/coq/coq/releases/download/V8.12%2Bbeta1/coq-8.12%2Bbeta1-reference-manual.pdf"
},
{
"name": "coq-8.12+beta1-installer-windows-i686-unsigned.exe",
"downloadUrl": "https://github.com/coq/coq/releases/download/V8.12%2Bbeta1/coq-8.12%2Bbeta1-installer-windows-i686-unsigned.exe"
},
{
"name": "coq-8.12+beta1-installer-windows-x86_64-unsigned.exe",
"downloadUrl": "https://github.com/coq/coq/releases/download/V8.12%2Bbeta1/coq-8.12%2Bbeta1-installer-windows-x86_64-unsigned.exe"
},
{
"name": "coq-8.12+beta1-installer-macos-unsigned.dmg",
"downloadUrl": "https://github.com/coq/coq/releases/download/V8.12%2Bbeta1/coq-8.12%2Bbeta1-installer-macos-unsigned.dmg"
}
]
}
},
{
"tag": {
"name": "V8.11.2"
},
"name": "Coq 8.11.2",
"description": "The Coq 8.11.2 release brings a few minor changes. See the [changelog](https://coq.github.io/doc/V8.11.2/refman/changes.html#changes-in-8-11-2).",
"url": "https://github.com/coq/coq/releases/tag/V8.11.2",
"isDraft": false,
"publishedAt": "2020-06-09T14:56:48Z",
"isPrerelease": false,
"releaseAssets": {
"nodes": [
{
"name": "coq-8.11.2-installer-windows-i686.exe",
"downloadUrl": "https://github.com/coq/coq/releases/download/V8.11.2/coq-8.11.2-installer-windows-i686.exe"
},
{
"name": "coq-8.11.2-installer-windows-x86_64.exe",
"downloadUrl": "https://github.com/coq/coq/releases/download/V8.11.2/coq-8.11.2-installer-windows-x86_64.exe"
},
{
"name": "coq-8.11.2-reference-manual.pdf",
"downloadUrl": "https://github.com/coq/coq/releases/download/V8.11.2/coq-8.11.2-reference-manual.pdf"
},
{
"name": "coq-8.11.2-installer-macos.dmg",
"downloadUrl": "https://github.com/coq/coq/releases/download/V8.11.2/coq-8.11.2-installer-macos.dmg"
}
]
}
},
{
"tag": {
"name": "V8.11.1"
},
"name": "Coq 8.11.1",
"description": "The most salient change in the 8.11.1 release is support for OCaml 4.10.0. See the [changelog](https://coq.github.io/doc/V8.11.1/refman/changes.html#changes-in-8-11-1) for more details.",
"url": "https://github.com/coq/coq/releases/tag/V8.11.1",
"isDraft": false,
"publishedAt": "2020-04-08T14:09:00Z",
"isPrerelease": false,
"releaseAssets": {
"nodes": [
{
"name": "coq-8.11.1-installer-windows-i686.exe",
"downloadUrl": "https://github.com/coq/coq/releases/download/V8.11.1/coq-8.11.1-installer-windows-i686.exe"
},
{
"name": "coq-8.11.1-installer-windows-x86_64.exe",
"downloadUrl": "https://github.com/coq/coq/releases/download/V8.11.1/coq-8.11.1-installer-windows-x86_64.exe"
},
{
"name": "coq-8.11.1-reference-manual.pdf",
"downloadUrl": "https://github.com/coq/coq/releases/download/V8.11.1/coq-8.11.1-reference-manual.pdf"
},
{
"name": "coq-8.11.1-installer-macos.dmg",
"downloadUrl": "https://github.com/coq/coq/releases/download/V8.11.1/coq-8.11.1-installer-macos.dmg"
}
]
}
},
{
"tag": {
"name": "V8.11.0"
},
"name": "Coq 8.11.0",
"description": "The main changes brought by Coq version 8.11 are:\r\n- **Ltac2**, a new tactic language for writing more robust larger scale\r\n tactics, with built-in support for datatypes and the multi-goal tactic monad.\r\n- **Primitive floats** are integrated in terms and follow the binary64 format\r\n of the IEEE 754 standard, as specified in the `Coq.Float.Floats` library.\r\n\r\nMany other cleanups and improvements have been performed and are further described in the [changelog](https://coq.github.io/doc/V8.11.0/refman/changes.html#version-8-11).\r\n\r\nSpecial note on **compatibility**:\r\n- **Fixed bugs** of `Export` and `Import` that can have a\r\n significant impact on user developments (**common source of\r\n incompatibility!**).\r\n",
"url": "https://github.com/coq/coq/releases/tag/V8.11.0",
"isDraft": false,
"publishedAt": "2020-01-30T07:03:58Z",
"isPrerelease": false,
"releaseAssets": {
"nodes": [
{
"name": "coq-8.11.0-installer-macos.dmg",
"downloadUrl": "https://github.com/coq/coq/releases/download/V8.11.0/coq-8.11.0-installer-macos.dmg"
},
{
"name": "coq-8.11.0-reference-manual.pdf",
"downloadUrl": "https://github.com/coq/coq/releases/download/V8.11.0/coq-8.11.0-reference-manual.pdf"
},
{
"name": "coq-8.11.0-installer-windows-i686.exe",
"downloadUrl": "https://github.com/coq/coq/releases/download/V8.11.0/coq-8.11.0-installer-windows-i686.exe"
},
{
"name": "coq-8.11.0-installer-windows-x86_64.exe",
"downloadUrl": "https://github.com/coq/coq/releases/download/V8.11.0/coq-8.11.0-installer-windows-x86_64.exe"
}
]
}
},
{
"tag": {
"name": "V8.11+beta1"
},
"name": "Coq 8.11+β1",
"description": "This is the first β version of Coq 8.11.\r\n\r\nThe main changes brought by Coq version 8.11 are:\r\n- **Ltac2**, a new tactic language for writing more robust larger scale\r\n tactics, with built-in support for datatypes and the multi-goal tactic monad.\r\n- **Primitive floats** are integrated in terms and follow the binary64 format\r\n of the IEEE 754 standard, as specified in the `Coq.Float.Floats` library.\r\n\r\nMany other cleanups and improvements have been performed and are further described in the changelog.\r\n\r\nSpecial note on **compability**:\r\n- **Fixed bugs** of `Export` and `Import` that can have a\r\n significant impact on user developments (**common source of\r\n incompatibility!**).\r\n",
"url": "https://github.com/coq/coq/releases/tag/V8.11%2Bbeta1",
"isDraft": false,
"publishedAt": "2019-12-06T13:17:59Z",
"isPrerelease": true,
"releaseAssets": {
"nodes": [
{
"name": "coq-8.11+beta1-installer-windows-i686.exe",
"downloadUrl": "https://github.com/coq/coq/releases/download/V8.11%2Bbeta1/coq-8.11%2Bbeta1-installer-windows-i686.exe"
},
{
"name": "coq-8.11+beta1-installer-macos.dmg",
"downloadUrl": "https://github.com/coq/coq/releases/download/V8.11%2Bbeta1/coq-8.11%2Bbeta1-installer-macos.dmg"
},
{
"name": "coq-8.11+beta1-installer-windows-x86_64.exe",
"downloadUrl": "https://github.com/coq/coq/releases/download/V8.11%2Bbeta1/coq-8.11%2Bbeta1-installer-windows-x86_64.exe"
},
{
"name": "coq-8.11+beta1-reference-manual.pdf",
"downloadUrl": "https://github.com/coq/coq/releases/download/V8.11%2Bbeta1/coq-8.11%2Bbeta1-reference-manual.pdf"
}
]
}
},
{
"tag": {
"name": "V8.10.2"
},
"name": "Coq 8.10.2",
"description": "Coq 8.10.2 brings a few bug fixes and documentation improvements, in particular:\r\n\r\n - Fixed a critical bug of template polymorphism and nonlinear universes\r\n - Fixed a few anomalies\r\n - Fixed an 8.10 regression related to the printing of coercions associated to notations\r\n - Fixed uneven dimensions of CoqIDE panels when window has been resized\r\n - Fixed queries in CoqIDE\r\n\r\nMore details can be found in the [reference manual](https://coq.github.io/doc/V8.10.2/refman/changes.html#changes-in-8-10-2).",
"url": "https://github.com/coq/coq/releases/tag/V8.10.2",
"isDraft": false,
"publishedAt": "2019-11-29T10:31:39Z",
"isPrerelease": false,
"releaseAssets": {
"nodes": [
{
"name": "coq-8.10.2-reference-manual.pdf",
"downloadUrl": "https://github.com/coq/coq/releases/download/V8.10.2/coq-8.10.2-reference-manual.pdf"
},
{
"name": "coq-8.10.2-installer-macos.dmg",
"downloadUrl": "https://github.com/coq/coq/releases/download/V8.10.2/coq-8.10.2-installer-macos.dmg"
},
{
"name": "coq-8.10.2-installer-windows-x86_64.exe",
"downloadUrl": "https://github.com/coq/coq/releases/download/V8.10.2/coq-8.10.2-installer-windows-x86_64.exe"
},
{
"name": "coq-8.10.2-installer-windows-i686.exe",
"downloadUrl": "https://github.com/coq/coq/releases/download/V8.10.2/coq-8.10.2-installer-windows-i686.exe"
}
]
}
},
{
"tag": {
"name": "V8.10.1"
},
"name": "Coq 8.10.1",
"description": "Coq 8.10.1 brings a few bug fixes and documentation improvements, in particular:\r\n\r\n - Fix proof of False when using SProp\r\n - Fix an anomaly when unsolved evar in Add Ring\r\n - Fix Ltac regression in binding free names in uconstr\r\n - Fix handling of unicode input before space\r\n - Fix custom extraction of inductives to JSON",
"url": "https://github.com/coq/coq/releases/tag/V8.10.1",
"isDraft": false,
"publishedAt": "2019-10-25T15:56:05Z",
"isPrerelease": false,
"releaseAssets": {
"nodes": [
{
"name": "coq-8.10.1-installer-macos.dmg",
"downloadUrl": "https://github.com/coq/coq/releases/download/V8.10.1/coq-8.10.1-installer-macos.dmg"
},
{
"name": "coq-8.10.1-installer-windows-x86_64.exe",
"downloadUrl": "https://github.com/coq/coq/releases/download/V8.10.1/coq-8.10.1-installer-windows-x86_64.exe"
},
{
"name": "coq-8.10.1-reference-manual.pdf",
"downloadUrl": "https://github.com/coq/coq/releases/download/V8.10.1/coq-8.10.1-reference-manual.pdf"
},
{
"name": "coq-8.10.1-installer-windows-i686.exe",
"downloadUrl": "https://github.com/coq/coq/releases/download/V8.10.1/coq-8.10.1-installer-windows-i686.exe"
}
]
}
},
{
"tag": {
"name": "V8.10.0"
},
"name": "Coq 8.10.0",
"description": "Coq 8.10.0 contains:\r\n\r\n - some quality-of-life bug fixes;\r\n - a critical bug fix related to template polymorphism;\r\n - native 63-bit machine integers;\r\n - a new sort of definitionally proof-irrelevant propositions: SProp;\r\n - private universes for opaque polymorphic constants;\r\n - string notations and numeral notations;\r\n - a new simplex-based proof engine for the tactics lia, nia, lra and nra;\r\n - new introduction patterns for SSReflect;\r\n - a tactic to rewrite under binders: under;\r\n - easy input of non-ASCII symbols in CoqIDE, which now uses GTK3.\r\n\r\nAll details can be found in the [user manual](https://coq.github.io/doc/V8.10.0/refman/changes.html#version-8-10).",
"url": "https://github.com/coq/coq/releases/tag/V8.10.0",
"isDraft": false,
"publishedAt": "2019-10-08T10:01:09Z",
"isPrerelease": false,
"releaseAssets": {
"nodes": [
{
"name": "coq-8.10.0-installer-macos.dmg",
"downloadUrl": "https://github.com/coq/coq/releases/download/V8.10.0/coq-8.10.0-installer-macos.dmg"
},
{
"name": "coq-8.10.0-installer-windows-i686.exe",
"downloadUrl": "https://github.com/coq/coq/releases/download/V8.10.0/coq-8.10.0-installer-windows-i686.exe"
},
{
"name": "coq-8.10.0-installer-windows-x86_64.exe",
"downloadUrl": "https://github.com/coq/coq/releases/download/V8.10.0/coq-8.10.0-installer-windows-x86_64.exe"
},
{
"name": "coq-8.10.0-reference-manual.pdf",
"downloadUrl": "https://github.com/coq/coq/releases/download/V8.10.0/coq-8.10.0-reference-manual.pdf"
}
]
}
},
{
"tag": {
"name": "V8.10+beta3"
},
"name": "Coq 8.10+β3",
"description": "This is the third β version of Coq 8.10.\r\n\r\nCompared to the previous one, it includes various bug fixes, including:\r\n\r\n - improved warning on coercion path ambiguity;\r\n - support for OCaml extraction of primitive machine integers;\r\n - fix for the soundness issue with template polymorphism;\r\n - fix extraction of dependent record projections to OCaml.\r\n\r\nMore details are given in the [user manual](https://coq.github.io/doc/v8.10/refman/changes.html#changes-in-8-10-beta3).",
"url": "https://github.com/coq/coq/releases/tag/V8.10%2Bbeta3",
"isDraft": false,
"publishedAt": "2019-09-16T12:28:25Z",
"isPrerelease": true,
"releaseAssets": {
"nodes": [
{
"name": "coq-8.10+beta3-installer-macos.dmg",
"downloadUrl": "https://github.com/coq/coq/releases/download/V8.10%2Bbeta3/coq-8.10%2Bbeta3-installer-macos.dmg"
},
{
"name": "coq-8.10+beta3-installer-windows-i686.exe",
"downloadUrl": "https://github.com/coq/coq/releases/download/V8.10%2Bbeta3/coq-8.10%2Bbeta3-installer-windows-i686.exe"
},
{
"name": "coq-8.10+beta3-installer-windows-x86_64.exe",
"downloadUrl": "https://github.com/coq/coq/releases/download/V8.10%2Bbeta3/coq-8.10%2Bbeta3-installer-windows-x86_64.exe"
},
{
"name": "coq-8.10+beta3-reference-manual.pdf",
"downloadUrl": "https://github.com/coq/coq/releases/download/V8.10%2Bbeta3/coq-8.10%2Bbeta3-reference-manual.pdf"
}
]
}
},
{
"tag": {
"name": "V8.10+beta2"
},
"name": "Coq 8.10+β2",
"description": "This is the second β version of Coq 8.10.\r\n\r\nCompared to the previous one, it includes many bug fixes and documentation improvements. In particular, CoqIDE instability on Windows has been addressed. [More details can be found in the manual.](https://coq.github.io/doc/v8.10/refman/changes.html#changes-in-8-10-beta2)",
"url": "https://github.com/coq/coq/releases/tag/V8.10%2Bbeta2",
"isDraft": false,
"publishedAt": "2019-06-20T07:42:12Z",
"isPrerelease": true,
"releaseAssets": {
"nodes": [
{
"name": "coq-8.10+beta2-installer-macos.dmg",
"downloadUrl": "https://github.com/coq/coq/releases/download/V8.10%2Bbeta2/coq-8.10%2Bbeta2-installer-macos.dmg"
},
{
"name": "coq-8.10+beta2-installer-windows-i686.exe",
"downloadUrl": "https://github.com/coq/coq/releases/download/V8.10%2Bbeta2/coq-8.10%2Bbeta2-installer-windows-i686.exe"
},
{
"name": "coq-8.10+beta2-installer-windows-x86_64.exe",
"downloadUrl": "https://github.com/coq/coq/releases/download/V8.10%2Bbeta2/coq-8.10%2Bbeta2-installer-windows-x86_64.exe"
},
{
"name": "coq-8.10+beta2-reference-manual.pdf",
"downloadUrl": "https://github.com/coq/coq/releases/download/V8.10%2Bbeta2/coq-8.10%2Bbeta2-reference-manual.pdf"
}
]
}
},
{
"tag": {
"name": "V8.9.1"
},
"name": "Coq 8.9.1",
"description": "Coq 8.9.1 contains\r\n- some quality-of-life bug fixes,\r\n- many improvements to the documentation,\r\n- a critical bug fix related to primitive projections and `native_compute`,\r\n- several additional Coq libraries shipped with the Windows installer.",
"url": "https://github.com/coq/coq/releases/tag/V8.9.1",
"isDraft": false,
"publishedAt": "2019-05-20T12:29:59Z",
"isPrerelease": false,
"releaseAssets": {
"nodes": [
{
"name": "coq-8.9.1-installer-macos.dmg",
"downloadUrl": "https://github.com/coq/coq/releases/download/V8.9.1/coq-8.9.1-installer-macos.dmg"
},
{
"name": "coq-8.9.1-installer-windows-i686.exe",
"downloadUrl": "https://github.com/coq/coq/releases/download/V8.9.1/coq-8.9.1-installer-windows-i686.exe"
},
{
"name": "coq-8.9.1-installer-windows-x86_64.exe",
"downloadUrl": "https://github.com/coq/coq/releases/download/V8.9.1/coq-8.9.1-installer-windows-x86_64.exe"
},
{
"name": "coq-8.9.1-reference-manual.pdf",
"downloadUrl": "https://github.com/coq/coq/releases/download/V8.9.1/coq-8.9.1-reference-manual.pdf"
}
]
}
},
{
"tag": {
"name": "V8.10+beta1"
},
"name": "Coq 8.10+β1",
"description": "This is the first β version of Coq 8.10.\r\n\r\nCoq 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](https://coq.github.io/doc/v8.10/refman/changes.html#version-8-10).\r\n\r\n**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:\r\n\r\n - CoqIDE does not work properly on Windows (issue #9885);\r\n - Template polymorphism breaks Prop/Set separation (issue #9294, proposed fix #9918).",
"url": "https://github.com/coq/coq/releases/tag/V8.10%2Bbeta1",
"isDraft": false,
"publishedAt": "2019-05-15T06:56:54Z",
"isPrerelease": true,
"releaseAssets": {
"nodes": [
{
"name": "coq-8.10+beta1-installer-macos.dmg",
"downloadUrl": "https://github.com/coq/coq/releases/download/V8.10%2Bbeta1/coq-8.10%2Bbeta1-installer-macos.dmg"
},
{
"name": "coq-8.10+beta1-installer-windows-x86_64.exe",
"downloadUrl": "https://github.com/coq/coq/releases/download/V8.10%2Bbeta1/coq-8.10%2Bbeta1-installer-windows-x86_64.exe"
},
{
"name": "coq-8.10+beta1-installer-windows-i686.exe",
"downloadUrl": "https://github.com/coq/coq/releases/download/V8.10%2Bbeta1/coq-8.10%2Bbeta1-installer-windows-i686.exe"
},
{
"name": "coq-8.10+beta1-reference-manual.pdf",
"downloadUrl": "https://github.com/coq/coq/releases/download/V8.10%2Bbeta1/coq-8.10%2Bbeta1-reference-manual.pdf"
}
]
}
}
]
}
}
}
}
Again, from this + a similar query for the Platform repository, we could consider auto-generating our releases data. The publication dates are accurate only starting at 8.7.
The text was updated successfully, but these errors were encountered:
Similarly to #3, regarding the releases, this request:
Again, from this + a similar query for the Platform repository, we could consider auto-generating our releases data. The publication dates are accurate only starting at 8.7.
The text was updated successfully, but these errors were encountered: