Coqpit.vim brings the interactivity and asynchronous of CoqIDE into Vim and Neovim.
This repository is fork of the-lambda-church/coquille.
Only Vim ( or Neovim ) and Coq.
- Vim ( 8.1 or above ) or Neovim
has('job') || has('nvim')
,has('lambda')
, ...
- Coq 8.6 or above. Checked versions below.
Please clone this repository to your vim runtimepath
or if you use plugin manager like dein.vim, add LumaKernel/coqpit.vim
repository.
Example for dein.vim
Add following to your toml file.
[[plugins]]
repo = "LumaKernel/coqpit.vim"
By default, coq will check the command coqidetop
followed by checking coqtop
.
However, if you want to use a specific version or executable,
set variable g:coqpit_coq_executable
in your .vimrc
.
Typically, you should specify {CoqInstallPath}/bin/coqidetop
or {CoqInstallPath}/bin/coqtop
for old versions.
To learn more flexible options, see :help coqpit-options
.
- Open coq file that typically ends with
.v
- Run
:CoqLaunch
( or writelet g:coqpit_auto_launch=1
in your.vimrc
) - Opening Infos/Goals buffers automatically.
Now, these commands can be used.
:CoqNext
- Forward one command.
:CoqBack
- Drop last command.
:CoqToCursor
- Forward to cursor.
:CoqToLast
- Forward to end of file.
- And other commands. See
:help coqpit-commands
.
function! MyCoqMaps()
nnoremap <silent> <C-C> :CoqLaunch<CR>
nnoremap <silent> <Leader>j :CoqNext<CR>
nnoremap <silent> <Leader>k :CoqBack<CR>
nnoremap <silent> <Leader>l :CoqToCursor<CR>
nnoremap <silent> <Leader>G :CoqToLast<CR>
nnoremap <silent> <Leader>g :CoqRerun<CR>
nnoremap <silent> <Leader>t :MoveToTop<CR>
nnoremap <silent> <Leader><F5> :CoqRefresh<CR>
nnoremap <Leader>compute :CoqQuery Compute .<Left>
nnoremap <Leader>print :CoqQuery Print .<Left>
nnoremap <Leader>check :CoqQuery Check .<Left>
nnoremap <Leader>se :CoqQuery Search ().<Left><Left>
endfunction
augroup my_coq
au!
au FileType coq :call MyCoqMaps()
augroup END
Recommended to define non-buffer local because these commands can be also used
from Infos/Goals buffers too. ( If not using coqpit_one_window=1
. )
Coqpit.vim will set the highligh colors automatically from backgrond color of your color scheme if you are using gui Vim.
- CoqChecked
- CoqCheckedAxiom
- CoqQueued
- CoqMarkedWarn
- CoqCheckedWarn
- CoqMarkedError
- CoqCheckedError
Needless to say, literally. Please check by yourself while using.
For more information, see :help coqpit-highlight-groups
This is example assuming for cterm with hybrid
color scheme.
hi CoqChecked ctermbg=17
hi CoqCheckedAxiom ctermbg=58
hi CoqQueued ctermbg=22
hi CoqMarkedWarn ctermbg=64
hi CoqCheckedWarn ctermbg=64
hi CoqMarkedError ctermbg=160
hi CoqCheckedError ctermbg=160
- Make your own Rearrange command.
- In that command,
- Use
b:coqpit_goal_bufnr
andb:coqpit_info_bufnr
to control Goals/Infos buffers. - If you are using
coqpit_one_window=1
option, use tablocal ( prefexedt:
) ones.
- Make your own Launch command.
- In that command,
- Run
:CoqLaunch
- Run your own Rearrange command.
Use your command or replace with original ones.
For concrete example, see :help coqpit-customize-window-example
.
To reset all Infos and Goals windows,
:bdelete
all not needed[Goals]
and[Infos]
buffers by yourself.
- or use
:CoqStopAll
command [or:call coqpit#stop_all()
]
- Run
:CoqRearrange
[or:call coqpit#reset_panels(1)
]
- on each window attached by coq file if you open multiple buffers and configure
one_window
is '0' - on each tab if you open multiple tabs
Or, reboot your Vim.
Like this.
let g:coqpit_coq_executable = '/c/Coq8.10/bin/coqidetop'
This is with g:coqpit_highlight_style_checked='last-line'
.
- With configure
g:coqpit_update_status_always
to0
, coq issues #9680 happens also in this plugin.- I recommend you NOT change this option. By default, working fine.
- If you use too many memory, coqpit fails with like an error message
Error: Out of memory
.- Refrain from using in unstable environment.
Welcome all issues and PRs. ( 日本語で issue を書くこともできます ; I welcome Japanse Issues as well. )
- the-lambda-church/coquille
- Original repository I forked and from which I use the name.
- coq syntax on vim.org
- coq indent on vim.org
- vital.vim
- vital-power-assert