From c0c80bb5b5c6d4d201a7b726749ab4aa11385a0d Mon Sep 17 00:00:00 2001 From: whonore Date: Mon, 21 Feb 2022 10:07:17 -0500 Subject: [PATCH 1/5] Remove Coq master CI workaround --- ci/coq.nix | 10 ---------- 1 file changed, 10 deletions(-) diff --git a/ci/coq.nix b/ci/coq.nix index bf287b36..129624c0 100644 --- a/ci/coq.nix +++ b/ci/coq.nix @@ -11,15 +11,5 @@ let (filter (s: s != "") (match "coq([0-9]|master)([0-9]*)-.*" tox_version)); in if dot_version == "8.4" then (import (fetchTarball url_8_4) { }).coq_8_4 -else if dot_version == "master" then - # NOTE: Temporary workaround until - # https://github.com/coq-community/coq-nix-toolbox/issues/95 is resolved - (pkgs.coq.override { version = dot_version; }).overrideAttrs (old: { - postInstall = old.postInstall + '' - for prog in $out/bin/coq*; do - wrapProgram $prog --prefix OCAMLPATH : $OCAMLPATH - done - ''; - }) else pkgs.coq.override ({ version = dot_version; }) From f3cdf46aae850fd538d187f4ef83a65ba4a5cdc3 Mon Sep 17 00:00:00 2001 From: whonore Date: Tue, 12 Jul 2022 12:20:17 -0400 Subject: [PATCH 2/5] Add Coq 8.16 to CI --- .github/workflows/ci.yml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index 119b294f..be5f2d43 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -14,7 +14,7 @@ jobs: runs-on: ubuntu-latest strategy: matrix: - coq_version: ['8.4', '8.5', '8.6', '8.7', '8.8', '8.9', '8.10', '8.11', '8.12', '8.13', '8.14', '8.15', 'master'] + coq_version: ['8.4', '8.5', '8.6', '8.7', '8.8', '8.9', '8.10', '8.11', '8.12', '8.13', '8.14', '8.15', '8.16', 'master'] py_version: [3.6] steps: - uses: actions/checkout@v2 From 4f56b567835ba37ac45331ca3f3470cd46dba83d Mon Sep 17 00:00:00 2001 From: whonore Date: Tue, 12 Jul 2022 12:41:18 -0400 Subject: [PATCH 3/5] Add Coq 8.16 to tox --- tox.ini | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/tox.ini b/tox.ini index 755065d6..34bca388 100644 --- a/tox.ini +++ b/tox.ini @@ -14,7 +14,7 @@ setenv = {[pybase]setenv} deps = {[pybase]deps} commands = python -m pytest -q tests/unit {posargs} -[testenv:coq{,84,85,86,87,88,89,810,811,812,813,814,815,master}-py{36}] +[testenv:coq{,84,85,86,87,88,89,810,811,812,813,814,815,816,master}-py{36}] description = Coq integration tests setenv = {[pybase]setenv} From 5e48728846c47e58809d10787a8ef239a459eed4 Mon Sep 17 00:00:00 2001 From: whonore Date: Tue, 12 Jul 2022 12:43:12 -0400 Subject: [PATCH 4/5] Add 8.16 XML interface --- python/xmlInterface.py | 5 +++++ 1 file changed, 5 insertions(+) diff --git a/python/xmlInterface.py b/python/xmlInterface.py index 59df4d32..4806c47f 100644 --- a/python/xmlInterface.py +++ b/python/xmlInterface.py @@ -1804,6 +1804,10 @@ def _standardize_add(self, res: Result) -> Result: return res +class XMLInterface816(XMLInterface815): + """The version 8.16.* XML interface.""" + + XMLInterfaces = ( ((8, 4, 0), (8, 5, 0), XMLInterface84), ((8, 5, 0), (8, 6, 0), XMLInterface85), @@ -1817,6 +1821,7 @@ def _standardize_add(self, res: Result) -> Result: ((8, 13, 0), (8, 14, 0), XMLInterface813), ((8, 14, 0), (8, 15, 0), XMLInterface814), ((8, 15, 0), (8, 16, 0), XMLInterface815), + ((8, 16, 0), (8, 17, 0), XMLInterface816), ) XMLInterfaceLatest = XMLInterfaces[-1][2] From 92f8c921f7fe5e2a77dee3c804f445e33225a5f0 Mon Sep 17 00:00:00 2001 From: whonore Date: Tue, 12 Jul 2022 12:44:03 -0400 Subject: [PATCH 5/5] Update documentation --- CHANGELOG.md | 4 ++++ README.md | 6 +++--- 2 files changed, 7 insertions(+), 3 deletions(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index ede17fa0..54c0ebf5 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -2,6 +2,10 @@ ## Unreleased ([master]) +### Added +- Support for Coq 8.16. + (PR #264) + ### Fixed - Highlight hypotheses separated by a comma on the first line of the hypotheses block in the Goal panel as `coqIdent`. diff --git a/README.md b/README.md index 9105e89e..c785e722 100644 --- a/README.md +++ b/README.md @@ -9,7 +9,7 @@ Coqtail enables interactive Coq proof development in Vim similar to [CoqIDE] or [ProofGeneral]. It supports: -- [Coq 8.4 - 8.15] +- [Coq 8.4 - 8.16] - Python >=3.6 (see [here](#python-2-support) for older versions) - Vim >=7.4 and Neovim >=0.3 - Simultaneous Coq sessions in different buffers @@ -46,7 +46,7 @@ Requirements: - Vim/Neovim compiled with `+python3` (3.6 or later) - Vim configuration options `filetype plugin on`, and optionally `filetype indent on` and `syntax on` (e.g. in `.vimrc`) -- [Coq 8.4 - 8.15] +- [Coq 8.4 - 8.16] Newer versions of Coq have not yet been tested, but should still work as long as there are no major changes made to the [XML protocol]. @@ -245,7 +245,7 @@ See [YouCompleteMe] for help building Vim with Python 3 support. If you cannot upgrade Vim, the [python2] branch still supports older Pythons. [python2]: https://github.com/whonore/Coqtail/tree/python2 -[Coq 8.4 - 8.15]: https://coq.inria.fr/download +[Coq 8.4 - 8.16]: https://coq.inria.fr/download [CoqIDE]: https://coq.inria.fr/refman/practical-tools/coqide.html [ProofGeneral]: https://proofgeneral.github.io/ [XML protocol]: https://github.com/coq/coq/blob/master/dev/doc/xml-protocol.md