Code Monkey home page Code Monkey logo

coqtail's Introduction

Coqtail

Code style: black Build Status

Interactive Coq Proofs in Vim

Coqtail enables interactive Coq proof development in Vim similar to CoqIDE or ProofGeneral.

It supports:

  • Coq 8.4 - 8.12
  • Python 21 and 3
  • Vim >=7.4 and Neovim >=0.3
  • Simultaneous Coq sessions in different buffers
  • Non-blocking communication between Vim and Coq (Vim >=8.0 and NeoVim only)

Installation and Requirements

As a vim package:

mkdir -p ~/.vim/pack/coq/start
git clone https://github.com/whonore/Coqtail.git ~/.vim/pack/coq/start/Coqtail
vim +helptags\ ~/.vim/pack/coq/start/Coqtail/doc +q

Using pathogen:

git clone https://github.com/whonore/Coqtail.git ~/.vim/bundle/Coqtail
vim +Helptags +q

Using Vundle:

Plugin 'whonore/Coqtail' (add this line in .vimrc)
vim +PluginInstall +qa

Using VimPlug:

Plug 'whonore/Coqtail' (add this line in .vimrc)
vim +PlugInstall +qa

Requirements:

  • Vim compiled with either +python1 or +python3
  • Vim configuration options filetype plugin on, and optionally filetype indent on and syntax on (e.g. in .vimrc)
  • Coq 8.4 - 8.12
  • The python3-distutils package.

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 Coqtail uses to communicate with coqtop.

Usage

Coqtail provides the following commands (see :help coqtail for more details):

Command Mapping Description
Starting and Stopping
CoqStart <leader>cc Launch Coqtail in the current buffer.
CoqStop <leader>cq Quit Coqtail in the current buffer.
CoqInterrupt CTRL-C Send SIGINT to coqtop.
Movement
{n}CoqNext <leader>cj Send the next n (1 by default) sentences to Coq.
{n}CoqUndo <leader>ck Step back n (1 by default) sentences.
{n}CoqToLine <leader>cl Send/rewind all sentences up to line n (cursor position by default). n can also be $ to check the entire buffer.
CoqToTop <leader>cT Rewind to the beginning of the file.
CoqJumpToEnd <leader>cG Move the cursor to the end of the checked region.
CoqGotoDef[!] <arg> <leader>cg Populate the quickfix list with possible locations of the definition of <arg> and try to jump to the first one. If your Vim supports 'tagfunc' you can also use CTRL-], :tag, and friends.
Queries
Coq <args> Send arbitrary queries to Coq (e.g. Check, About, Print, etc.).
Coq Check <arg> <leader>ch Show the type of <arg> (the mapping will use the term under the cursor or the highlighted range in visual mode).
Coq About <arg> <leader>ca Show information about <arg>.
Coq Print <arg> <leader>cp Show the definition of <arg>.
Coq Locate <arg> <leader>cf Show where <arg> is defined.
Coq Search <args> <leader>cs Show theorems about <args>.
Panel Management
CoqRestorePanels <leader>cr Re-open the Goal and Info panels.
{n}CoqGotoGoal <leader>cgg Scroll the Goal panel to the start of the nth goal (defaults to 1). Number of lines shown is controlled by g:coqtail_goal_lines.
{n}CoqGotoGoal! <leader>cGG Scroll the Goal panel to the end of the nth goal.
CoqGotoGoalNext g] Scroll the Goal panel to the start of the next goal.
CoqGotoGoalNext! G] Scroll the Goal panel to the end of the next goal.
CoqGotoGoalPrev g[ Scroll the Goal panel to the start of the previous goal.
CoqGotoGoalPrev! G[ Scroll the Goal panel to the end of the previous goal.

Configuration

Mappings

The mappings above are set by default, but you can disable them all and define your own by setting g:coqtail_nomap = 1 in your .vimrc. Some of the commands, such as CoqNext, also have insert-mode mappings by default, which can be disabled with g:coqtail_noimap. Alternatively, you can keep the defaults but remap specific commands. For example, use map <leader>ci <Plug>CoqInterrupt to avoid hijacking CTRL-C. The <leader>c prefix may be inconvenient depending on your mapleader setting. In that case you can set a custom prefix with g:coqtail_map_prefix (or g:coqtail_imap_prefix for just insert-mode mappings).

Coq Executable

By default Coqtail uses the first coq(ide)top(.opt) found in your PATH. Use b:coqtail_coq_path (or g:coqtail_coq_path) to specify a different directory to search in. You can also override the name of the Coq executable to use with b:coqtail_coq_prog (or g:coqtail_coq_prog). For example, to use the HoTT library:

let b:coqtail_coq_path = '/path/to/HoTT'
let b:coqtail_coq_prog = 'hoqidetop'

_CoqProject

Coqtail understands and will search for _CoqProject files on :CoqStart. Additional or different project files can be specified with g:coqtail_project_files. For example, to include arguments from both _CoqProject and _CoqProject.local:

let g:coqtail_project_files = ['_CoqProject', '_CoqProject.local']

Syntax Highlighting and Indentation

Coqtail also comes with an ftdetect script for Coq, as well as modified versions of Vincent Aravantinos' syntax and indent scripts for Coq. These scripts are used by default but can be disabled by setting g:coqtail_nosyntax = 1 and g:coqtail_noindent = 1 respectively. Formatting of comments can be disabled with g:coqtail_noindent_comment.

See :help coqtail-configuration for more configuration variables.

Vim Plugin Interoperability

Jumping between matches

Coqtail defines b:match_words patterns to support jumping between matched text with % using the matchup or matchit plugins.

Automatically closing blocks

Coqtail defines patterns to enable automatic insertion of the appropriate End command for code blocks such as Sections, Modules, and match expressions with endwise.

Thanks

Parts of Coqtail were originally inspired by/adapted from Coquille (MIT License, Copyright (c) 2013, Thomas Refis).


Because Python 2 has reached its end-of-life and supporting it alongside Python 3 makes it difficult to improve and maintain the code, Coqtail will drop support for Python 2 in the near future. At that time a stable version will be tagged and all future versions will be Python 3-only. See YouCompleteMe for help building Vim with Python 3 support.

coqtail's People

Contributors

andres-erbsen avatar andres-erbsen-sifive avatar cypher1 avatar j-hui avatar licynthiax avatar lysxia avatar mbodin avatar tomtomjhj avatar whonore avatar

Recommend Projects

  • React photo React

    A declarative, efficient, and flexible JavaScript library for building user interfaces.

  • Vue.js photo Vue.js

    ๐Ÿ–– Vue.js is a progressive, incrementally-adoptable JavaScript framework for building UI on the web.

  • Typescript photo Typescript

    TypeScript is a superset of JavaScript that compiles to clean JavaScript output.

  • TensorFlow photo TensorFlow

    An Open Source Machine Learning Framework for Everyone

  • Django photo Django

    The Web framework for perfectionists with deadlines.

  • D3 photo D3

    Bring data to life with SVG, Canvas and HTML. ๐Ÿ“Š๐Ÿ“ˆ๐ŸŽ‰

Recommend Topics

  • javascript

    JavaScript (JS) is a lightweight interpreted programming language with first-class functions.

  • web

    Some thing interesting about web. New door for the world.

  • server

    A server is a program made to process requests and deliver data to clients.

  • Machine learning

    Machine learning is a way of modeling and interpreting data that allows a piece of software to respond intelligently.

  • Game

    Some thing interesting about game, make everyone happy.

Recommend Org

  • Facebook photo Facebook

    We are working to build community through open source technology. NB: members must have two-factor auth.

  • Microsoft photo Microsoft

    Open source projects and samples from Microsoft.

  • Google photo Google

    Google โค๏ธ Open Source for everyone.

  • D3 photo D3

    Data-Driven Documents codes.