Coq 8.20 (#373)

* Support Coq 8.20

* Update GitHub Actions

* Highlight and indent Rewrite Rule

.github/workflows/coq-tests.yml

@@ -43,23 +43,24 @@ jobs:
           - '8.17'
           - '8.18'
           - '8.19'
+          - '8.20'
           - 'master'
         py_version: ['3.6']
     steps:
       - uses: actions/checkout@v4
       - name: Install Nix
-        uses: cachix/install-nix-action@v25
+        uses: cachix/install-nix-action@v27
         with:
           nix_path: nixpkgs=channel:nixpkgs-unstable
       - name: Install Cachix
-        uses: cachix/cachix-action@v14
+        uses: cachix/cachix-action@v15
         with:
           name: coq
           skipPush: true
       - name: Set up Nix cache
         # Only Coq master needs additional caching.
         if: ${{ matrix.coq_version == 'master' }}
-        uses: DeterminateSystems/magic-nix-cache-action@v2
+        uses: DeterminateSystems/magic-nix-cache-action@v8
       - name: Install Coq ${{ matrix.coq_version }}
         run: nix-env -j auto --cores 0 -i -f ci/coq.nix --argstr version ${{ matrix.coq_version }}
       - name: Install Python ${{ matrix.py_version }}

.github/workflows/vim-tests.yml

@@ -32,11 +32,11 @@ jobs:
     steps:
       - uses: actions/checkout@v4
       - name: Install Nix
-        uses: cachix/install-nix-action@v25
+        uses: cachix/install-nix-action@v27
         with:
           nix_path: nixpkgs=channel:nixos-20.09
       - name: Install Cachix
-        uses: cachix/cachix-action@v14
+        uses: cachix/cachix-action@v15
         with:
           name: whonore-vim
           skipPush: true

CHANGELOG.md

@@ -2,6 +2,10 @@
 
 ## Unreleased ([main])
 
+### Added
+- Basic support for `Rewrite Rule` syntax highlighting and indentation.
+  (PR #373)
+
 ### Fixed
 - Correctly execute commands containing quotes (e.g., `Coq Check a'`).
   (PR #371)

README.md

@@ -11,7 +11,7 @@ Coqtail enables interactive Coq proof development in Vim similar to [CoqIDE] or
 [ProofGeneral].
 
 It supports:
-- [Coq 8.4 - 8.19]
+- [Coq 8.4 - 8.20]
 - Python >=3.6 (see [here](#python-2-support) for older versions)
 - Vim >=7.4 and Neovim >=0.3
 - Simultaneous Coq sessions in different buffers
@@ -49,7 +49,7 @@ vim +PlugInstall +qa
 - Vim compiled with `+python3` (3.6 or later) or the `pynvim` Python package for Neovim
 - Vim configuration options `filetype plugin on`, and optionally `filetype
   indent on` and `syntax on` (e.g. in `.vimrc`)
-- [Coq 8.4 - 8.19]
+- [Coq 8.4 - 8.20]
 
 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].
@@ -306,7 +306,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.19]: https://coq.inria.fr/download
+[Coq 8.4 - 8.20]: 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

indent/coq.vim

@@ -41,6 +41,8 @@ let s:bullet = '[-+*]\+)\@!'
 let s:bulletline = '^\s*' . s:bullet
 let s:match = '\<\%(lazy\|multi\)\?match\>'
 let s:inductive = '\%(\%(Co\)\?Inductive\|Variant\)'
+let s:rewrite = '\<Rewrite\_s\+Rule\>'
+let s:vbar_cmd = '\%(' . s:inductive . '\|' . s:rewrite . '\)'
 let s:lineend = '\s*$'
 
 " Match syntax groups.
@@ -243,7 +245,7 @@ function! s:GetCoqIndent() abort
   if l:currentline =~# '^\s*|[|}]\@!'
     let l:match = s:indent_of_previous_pair(s:match, '', '\<end\>', 1, ['string', 'comment'])
     let l:off = get(g:, 'coqtail_inductive_shift', 1) * &sw
-    return l:match != -1 ? l:match : s:indent_of_previous('^\s*' . s:inductive) + l:off
+    return l:match != -1 ? l:match : s:indent_of_previous('^\s*' . s:vbar_cmd) + l:off
   endif
 
   " current line begins with terminating '|}', '}', or ')'

syntax/coq.vim

@@ -267,7 +267,7 @@ syn region coqBinderTypeParen   contained contains=@coqTerm matchgroup=coqVernac
 syn region coqBinderTypeCurly   contained contains=@coqTerm matchgroup=coqVernacPunctuation start=":" end="}"
 
 " Declarations
-syn region coqDecl       contains=coqIdent,coqDeclTerm,coqBinder matchgroup=coqVernacCmd start="\<\%(Axioms\?\|Conjectures\?\|Hypothes[ie]s\|Parameters\?\|Variables\?\|Context\)\>" matchgroup=coqVernacCmd end="\.\_s" keepend
+syn region coqDecl       contains=coqIdent,coqDeclTerm,coqBinder matchgroup=coqVernacCmd start="\<\%(Axioms\?\|Conjectures\?\|Hypothes[ie]s\|Parameters\?\|Variables\?\|Context\|Symbols\?\)\>" matchgroup=coqVernacCmd end="\.\_s" keepend
 syn region coqDeclTerm   contained contains=@coqTerm matchgroup=coqVernacPunctuation start=":" end=")"
 syn region coqDeclTerm   contained contains=@coqTerm matchgroup=coqVernacPunctuation start=":" end="\.\_s"
 
@@ -491,6 +491,9 @@ syn region elpiString contained start=+"+ skip=+\\"+ end=+"+ extend
 syn match elpiMode contained "\<[io]:"
 syn match elpiNumber contained "[0-9]\+"
 
+" Rewrite Rules
+syn region coqRewrite contains=coqIdent,coqVernacPunctuation,coqLtacContents matchgroup=coqVernacCmd start="\<Rewrite\_s\+Rule\>" end="\.\_s" keepend
+
 " Various (High priority)
 syn region  coqComment           containedin=ALLBUT,coqString contains=coqComment,coqTodo,@Spell start="(\*" end="\*)" extend keepend
 syn keyword coqTodo              contained TODO FIXME XXX NOTE

tests/vim/indent.vader

@@ -90,6 +90,25 @@ Expect coq (indented-inductive-shift):
 Execute (indent-inductive-shift-option-post):
   unlet g:coqtail_inductive_shift
 
+Given coq (rewrite):
+  Rewrite Rule pplus_rewrite :=
+  | ?n ++ 0 => ?n
+  | ?n ++ S ?m =>
+  S (?n ++ ?m)
+  | 0 ++ ?n => ?n
+  | S ?n ++ ?m => S (?n ++ ?m).
+
+Do (indent-rewrite):
+  =ip
+
+Expect coq (indented-rewrite):
+  Rewrite Rule pplus_rewrite :=
+    | ?n ++ 0 => ?n
+    | ?n ++ S ?m =>
+        S (?n ++ ?m)
+    | 0 ++ ?n => ?n
+    | S ?n ++ ?m => S (?n ++ ?m).
+
 Given coq (match):
   Definition f (b : bool) :=
   match b with

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,816,817,818,819,master}-py{36}]
+[testenv:coq{,84,85,86,87,88,89,810,811,812,813,814,815,816,817,818,819,820,master}-py{36}]
 description = Coq integration tests
 setenv =
     {[pybase]setenv}