Commit 571969d5 authored by Manu Beffara's avatar Manu Beffara
Browse files

First functional version.

parents
/doc/tags
Coq-au-Vim
==========
Coq-au-Vim is a Vim plugin for working with the [Coq](https://coq.inria.fr/)
proof assistant. It provides motions, folding and communication with Coq for
interactive proof development.
Requirements
------------
Coq-au-Vim requires
- Vim version 8
- Coq version 8.6
Prior versions of Vim will not be supported because version 8 is the one that
introduces asynchronous communication with external tools. For older versions
of Vim, use [Coquille](https://github.com/the-lambda-church/coquille), which
works well with Coq up to version 8.5.
Installation
------------
This repository is directly usable as a plugin using the package system of
Vim 8. You can install it by cloning it as a package subdirectory, by doing
mkdir -p ~/.vim/pack/coq/start
cd ~/.vim/pack/coq/start
git clone https://manu@framagit.org/manu/coq-au-vim.git
This assumes that your base Vim directory is `~/.vim` and puts the plugin in a
package named `coq`, but any other package name can be used.
Run the following Vim command to register the help file:
:helptags ALL
Syntax highlighting and indent scripts are not included, I recommend using
those by Vincent Aravantinos and packaged by Jeremy Voorhis, by doing:
cd ~/.vim/pack/coq/start
git clone https://github.com/jvoorhis/coq.vim
Usage
-----
Full documentation is included with the plugin, say `:help coq.txt` from
within Vim to display the help file. For interaction with Coq, the following
commands are provided:
- `:CoqStart` starts an interactive session and defines the other commands,
- `:CoqQuit` ends the current interactive session,
- `:CoqNext` sends the next sentence to Coq,
- `:CoqRewind` rewinds by one sentence,
- `:CoqToCursor` sends or rewinds up to the current cursor position.
Key mappings compatible with CoqIDE are installed by the `:CoqStart`
command.
This diff is collapsed.
*coq.txt* Syntax support and interactive development with Coq
vim:ft=help:tw=78:ts=8:sw=8:et
___ __ ___ ~
/ __|___ __ _ __ _ _ _ \ \ / (_)_ __ ~
| (__/ _ \/ _` |__/ _` | || |__\ V /| | ' \ ~
\___\___/\__, | \__,_|\_,_| \_/ |_|_|_|_|~
|_| ~
=============================================================================
Contents
1. Introduction .............................. |coq-intro|
2. Editing Coq files ......................... |coq-editing|
3. Interactive theorem proving ............... |coq-ide|
3.1. Commands ............................ |coq-commands|
3.2. Key mappings ........................ |coq-mappings|
4. Configuration ............................. |coq-config|
5. Contributing .............................. |coq-contributing|
6. Credits ................................... |coq-credits|
=============================================================================
1. Introduction *coq-intro*
This plugin provides a environment for working with the Coq theorem prover.
It provides |filetype| support for editing Coq source files and a mode for
interactive proof development, in the style of the standard Coq IDE.
The interactive mode requires Vim version 8 and Coq version 8.6.
=============================================================================
2. Editing Coq files *coq-editing*
*coq-syntax*
Coq-au-Vim does not provide syntax highlighting or indent support for Coq
files because it can be found in other packages. I recommend using the scripts
originally written by Vincent Aravantinos and packaged by Jeremy Voorhis:
https://github.com/jvoorhis/coq.vim
This package only provides Coq-aware motions and folding.
*coq-motions*
Standard motions are adapted for Coq files: a sentence is interpreted in the
sense of Coq, so that standard key mappings work as expected.
*coq-(*
( [count] sentences backward.
*coq-)*
) [count] sentences forward.
*coq-text-object*
The following motions override the default ones for text selection, using
definitions adapted to Coq source files.
*coq-v_as*
as "a sentence", select the current sentence including the
following whitespace. Visual characterwise mode.
*coq-v_is*
is "inner sentence", select the current sentence excluding
surrounding whitespace. Visual characterwise mode.
*coq-folding*
Coq-au-Vim provides a folding function for Coq files that has the following
behaviour:
all proofs are marked as folds (from "Proof." to the matching "Qed."),
all section headers (in the sense of coqdoc, i.e. following the coqdoc
markup conventions for comments) are folds at level 1, so that a
completely folded document with such sections appears as a table of
contents.
The plugin defines the 'foldexpr' and 'foldtext' options but does not set
'foldmethod' to "expr". This feature can be activated by simply saying
setlocal foldmethod=expr
in a Coq buffer (or as an |autocommand|).
=============================================================================
3. Interactive theorem proving *coq-ide*
The following commands and key bindings provide an interactive proving
environment using the Coq top-level. The way it works is directly inspired by
the standard Coq IDE.
Each buffer can have its own interactive session. Since a session uses a
particular window layout for interaction, running several sessions in parallel
works best with one |tab-page| per session.
-----------------------------------------------------------------------------
3.1. Commands *coq-commands*
Only |:CoqStart| is automatically defined in Coq buffers, the other commands
are defined when starting a session and undefined when closing a session.
*:CoqStart*
:CoqStart Start a Coq interpreter associated with the current buffer and
setup windows for interaction: one window for the current
proof goals and one window for informational messages.
*:CoqQuit*
:CoqQuit Stop the Coq interpreter associated with the current buffer
and close the goal and information windows.
*:CoqNext*
:CoqNext Send the next sentence to Coq and check it.
*:CoqRewind*
:CoqRewind Rewind by one sentence.
*:CoqToCursor*
:CoqToCursor Check sentences or rewind, so that the last sentence before
the cursor is checked.
-----------------------------------------------------------------------------
3.2. Key mappings *coq-mappings*
The following key mappings are defined locally for a Coq buffers when the
|:CoqStart| command is called and removed when the |:CoqQuit| command is
called. They apply in all modes.
*coq-<C-Down>*
<C-Down> Check the next sentence, alias for |:CoqNext|.
*coq-<C-Up>*
<C-Up> Rewind by one sentence, alias for |:CoqRewind|.
*coq-<C-Right>*
<C-Right> Check or rewind up to the position of the cursor, alias for
|:CoqToCursor|.
Interaction with the Coq top-level is asynchronous, so you can continue using
Vim while Coq is processing sentences.
However, editing in a previously checked zone currently does not rewind
automatically.
=============================================================================
4. Configuration *coq-config*
The interactive proof mode currently has no configuration options, except for
enabling debugging, see |coq-debugging| for details.
Folding can be activated by setting 'foldmethod' to expr, see |coq-folding|.
The Coq highlight groups used for feedback from the Coq top-level are the
following:
*hl-CoqSent*
CoqSent the region that was sent, before it is accepted
*hl-CoqAdded*
CoqAdded regions that have been sent and accepted
*hl-CoqChecked*
CoqChecked regions that have been successfully processed
*hl-CoqError*
CoqError errors detected by Coq
By default CoqError is linked to Error and the other have a red-ish,
yellow-ish or green-ish background.
=============================================================================
5. Contributing *coq-contributing*
Any feedback is welcome, in the form of suggestions, bug reports or patches.
The public Git repository of the project can be found at
https://git.framasoft.org/manu/coq-au-vim
*coq-debugging*
The Coq interaction plugin can be run in debugging mode by setting the
*b:coq_debug* variable. In this case, an extra window will be open on startup
and debugging messages will be appended there. The *b:coq_debug* variable is
expected to be string, the presence of each letter below will trigger the
display of a particular kind of information
letter messages written in the debug window~
e protocol errors (unrecognized messages from coqtop)
f feedback items
j job management (starting and stopping coqtop)
m parsed messages from coqtop
r requests to coqtop and answers
t put a timestamp in front of each line in the log
x raw XML messages exchanged with coqtop
=============================================================================
6. Credits *coq-credits*
The plugin was written from scratch for Vim 8 and Coq 8.6 but with direct
inspiration from Coquille by Thomas Refis <https://github.com/trefis>:
https://github.com/the-lambda-church/coquille
The name was taken from a comment on Reddit by someone wondering why no one
had yet used this name for a Vim plugin for Coq support. Now the name is used!
" = Motions = {{{1
" Search forward for a pattern, skipping comments. The return value is the
" number of the first maching sub-expression (as for the Vim function search()
" with the 'p' option). The second argument indicates whether a match at the
" current position is accepted.
function! s:SearchForward (pattern, immediate)
let immediate = a:immediate
while v:true
let result = search('\((\*\)\|\(\*)\)\|' . a:pattern,
\ immediate ? 'cepWz' : 'epWz')
if result < 2
return result
elseif result > 3
return result - 2
elseif result == 3
" A closing comment delimiter was found, ignore it.
let immediate = v:false
continue
endif
" A comment was found, skip it and retry.
let level = 1
while level > 0
let result = search('(\*\|\(\*)\)', 'epWz')
if result == 0
" A comment is left open at the end of the buffer.
return 0
elseif result == 1
" An opening delimiter was found.
let level += 1
else
" A closing delimiter was found.
let level -= 1
endif
endwhile
let immediate = v:false
endwhile
endfunction
" Search backward for a pattern, skipping comments. The return value is the
" number of the first maching sub-expression (as for the Vim function search()
" with the 'p' option). The second argument indicates whether a match at the
" current position is accepted.
function! s:SearchBackward (pattern, immediate)
let immediate = a:immediate
while v:true
let result = search('\((\*\)\|\(\*)\)\|' . a:pattern,
\ immediate ? 'bcpW' : 'bpW')
if result < 2
return result
elseif result > 3
return result - 2
elseif result == 2
" An opening comment delimiter was found, ignore it.
let immediate = v:false
continue
endif
" A comment was found, skip it and retry.
let level = 1
while level > 0
let result = search('(\*\|\(\*)\)', 'bpW')
if result == 0
" A comment is left open at the beginning of the buffer.
return 0
elseif result == 1
" An opening delimiter was found.
let level -= 1
else
" A closing delimiter was found.
let level += 1
endif
endwhile
let immediate = v:false
endwhile
endfunction
" Check if the current position is a beginning of sentence, i.e. if it is
" located between a period or bullet and the next non-blank character. The
" argument indicates how the cursor is considered:
" - if true, a period or bullet under the cursor is accepted but the first
" non-blank character of a sentence is refused,
" - if false, the cursor position is accepted even if it contains the first
" non-blank character of a sentence.
function! s:IsBeginningOfSentence (immediate)
let immediate = a:immediate
let position = getpos(".")
while v:true
let result = s:SearchBackward('\.\_s\|\([-+*{}]\)\|\(\S\)', immediate)
if result <= 1
" A period or the beginning of the buffer was found.
call setpos(".", position)
return v:true
elseif result == 2
" A potential bullet was found, validate it by checking it is a
" beginning of sentence.
let immediate = v:false
continue
else
" Something else was found before.
call setpos(".", position)
return v:false
endif
endwhile
endfunction
" Move to the next period or bullet. Return v:true if one was found, v:false
" otherwise (i.e. when the end of the buffer was reached). The argument
" indicates whether a match at the current position is accepted.
function! CoqNextPeriod (immediate)
let immediate = a:immediate
while v:true
let result = s:SearchForward('\.\_s\@=\|\([-+*{}]\)', immediate)
if result == 2
" A potential bullet was found, check it.
if s:IsBeginningOfSentence(v:false)
return v:true
endif
else
return result != 0
endif
let immediate = v:false
endwhile
endfunction
" Move to the previous period or bullet. Return v:true if one was found,
" v:false otherwise (i.e. when the beginning of the buffer was reached).
function! CoqPreviousPeriod (immediate)
let immediate = a:immediate
while v:true
let result = s:SearchBackward('\.\_s\|\([-+*{}]\)', immediate)
if result == 2
" A potential bullet was found, check it.
if s:IsBeginningOfSentence(v:false)
return v:true
endif
else
return result != 0
endif
let immediate = v:false
endwhile
endfunction
" Move to the next sentence. The 'count' argument indicates how many sentences
" to advance. Return v:true if a next sentence was found, v:false otherwise.
function! CoqNextSentence (count)
if !s:IsBeginningOfSentence(v:true)
call CoqNextPeriod(v:true)
endif
let i = a:count
while i > 1
if !CoqNextPeriod(v:false)
return v:false
endif
let i -= 1
endwhile
return s:SearchForward('\S', v:false) != 0
endfunction
" Move the the beginning of the current sentence, or the previous one if the
" cursor is already at the beginning of a sentence. The 'count' argument
" indicates how many sentences to advance. Return v:true if a proper previous
" sentence was found, v:false otherwise.
function! CoqPreviousSentence (count)
if s:IsBeginningOfSentence(v:false)
call CoqPreviousPeriod(v:false)
endif
let i = a:count
while i > 1
if !CoqPreviousPeriod(v:false)
return v:false
endif
let i -= 1
endwhile
return s:SearchForward('\S', !CoqPreviousPeriod(v:false)) != 0
endfunction
" Select a sentence in visual mode.
function! CoqVisualSentence (inner)
let [l, c] = getpos(".")[1:2]
if s:IsBeginningOfSentence(v:true)
\ && stridx(' .-+*', strcharpart(getline(l), c - 1, 1)) <= 0
" The cursor is on a blank between a period and the next sentence:
" - if inner is true, select the blanks between the period ans the
" sentence,
" - if inner is false, select also the next sentence.
if CoqPreviousPeriod(v:false)
call s:SearchForward('\s', v:false)
endif
" call setpos("'<", getpos("."))
normal v
if a:inner
call s:SearchForward('\s\S\@=', v:true)
else
call CoqNextPeriod(v:false)
endif
else
" The cursor is in a sentence. Select the sentence, plus the following
" space if inner is false.
if CoqPreviousPeriod(v:false)
call s:SearchForward('\S', v:false)
endif
" call setpos("'<", getpos("."))
normal v
call CoqNextPeriod(v:true)
if !a:inner
call s:SearchForward('\s\S\@=', v:true)
endif
endif
call setpos("'>", getpos("."))
endfunction
" = Folding = {{{1
function! CoqFoldLevel (lnum)
let line = getline(a:lnum)
if line =~ "(\\*\\* \\*\\+ "
return ">1"
elseif line =~ "^ \\*{2,} "
return ">1"
elseif line ==# "Proof."
return ">2"
elseif line =~# "^\\(Qed\\|Defined\\|Abort\\|Admitted\\)."
return "<2"
endif
return "="
endfunction
function! CoqFoldText ()
let text = getline(v:foldstart)
if text =~ "\\((\\*\\* \\| \\)\\*\\+ "
if strpart(text, 0, 4) == "(** "
let text = strpart(text, 4)
else
let text = strpart(text, 2)
endif
let text = substitute(text, " *\\(\\*)\\)\\?$", "", "")
let level = stridx(text, " ")
let text = "--[ " . strpart(text, level + 1) . " ]"
while level > 1
let text = "---" . text
let level = level - 1
endwhile
return text
else
return "-- " . text . " "
endif
endfunction
" = Commands and mappings = {{{1
command! -buffer CoqStart :call coqtop#Start()
nnoremap <buffer> <silent> ( :<C-U>call CoqPreviousSentence(v:count)<CR>
nnoremap <buffer> <silent> ) :<C-U>call CoqNextSentence(v:count)<CR>
vnoremap <buffer> <silent> is :<C-U>call CoqVisualSentence(v:true)<CR>
vnoremap <buffer> <silent> as :<C-U>call CoqVisualSentence(v:false)<CR>
setlocal shiftwidth=2 tabstop=2 expandtab
setlocal foldexpr=CoqFoldLevel(v:lnum) foldtext=CoqFoldText()
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment