Coqpit.vim

Coqpit.vim brings the interactivity and asynchronous of CoqIDE into Vim and Neovim.

This repository is fork of the-lambda-church/coquille.

Dependencies

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.
  • Coq8.5pl3
  • Coq8.6
  • Coq8.7
  • Coq8.9
  • Coq8.10
  • Coq8.11
  • Recomended to use newer and more stable version.

Installation

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"

Specifying coq executable

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 .

Getting started

1. Open coq file that typically ends with .v
2. Run :CoqLaunch ( or write let g:coqpit_auto_launch=1 in your .vimrc )
3. 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 .

Mapping Examples

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. )

Configuration Highlight Colors

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

Example for highlight config

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

Customize window locations

1. Make your own Rearrange command.
2. In that command,

• Use b:coqpit_goal_bufnr and b:coqpit_info_bufnr to control Goals/Infos buffers.
• If you are using coqpit_one_window=1 option, use tablocal ( prefexed t: ) ones.

3. Make your own Launch command.
4. In that command,
5. Run :CoqLaunch
6. Run your own Rearrange command.

Use your command or replace with original ones.

For concrete example, see :help coqpit-customize-window-example .

F.A.Q.

Messed up Infos and Goals windows!

To reset all Infos and Goals windows,

1. :bdelete all not needed [Goals] and [Infos] buffers by yourself.

• or use :CoqStopAll command [or :call coqpit#stop_all()]

2. 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.

I want to pass the path in Windows MSYS2.

Like this.

let g:coqpit_coq_executable = '/c/Coq8.10/bin/coqidetop'

Screenshoots

This is with g:coqpit_highlight_style_checked='last-line'.

Known Issues

• With configure g:coqpit_update_status_always to 0, 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.

License

ISC License

Contribution

Welcome all issues and PRs. ( 日本語で issue を書くこともできます ; I welcome Japanse Issues as well. )

Thanks

• 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