17
$\begingroup$

I remember the last time I was trying to get into proof assistants, I was discouraged by the lack of functionality for vim users. At the time, it seemed like a lot of powerful features (holes, etc) worked best with Emacs, and had only limited support (if any support at all) in vim. Unfortunately, this was so discouraging that I never actually learned how to use any theorem provers (I'm aware of evil, but it also seemed like a hassle).

But now a few years have passed, and with the growing popularity of Neovim (which adds a lot of modern functionality), it seems reasonable that the state of things might have changed (or at least, that it might be changing). As some evidence for this, I saw a recent blog post about cornelis, which promises to bring many of the Agda features from Emacs to Neovim.

I'm excited about theorem provers again, and seeing this blog post has given me hope that there might be other resources for vim users that I wasn't able to find with a cursory google (even googling "cornelius agda" doesn't bring up the above project on the first page). Which brings me to the main question I have:

If you are a (Neo)vim user, which theorem prover(s) do you use? Moreover, how do you interact with it? Does the experience feel fully featured?

If there are any nice guides on getting things up and running for a Vim user, I would also be interested in those. The nice thing about being new to all this is that I'm currently language-agnostic, and I would be happy to learn any of the major languages.

Thanks in advance! ^_^

Improve this question
$\endgroup$
0

3 Answers 3

Reset to default
10
$\begingroup$

Neovim support in Lean has come a long way recently: The Neovim plugin (by Julian Berman, Rishikesh Vaishnav and Gabriel Ebner predominantly) supports both Lean 3 and Lean 4 and supports both foundational and advanced features (the infoview, widgets, hole commands, Unicode replacement). Neovim version 0.6 or higher is required.

The only feature of the VSCode plugin that I have not yet seen replicated with lean.nvim is support for rendering arbitrary HTML, this is not a particularly everyday feature of most Lean workflows (yet). But there some nice examples such as the Rubik's Cube info-view display at https://github.com/kendfrey/rubiks-cube-group.

Previously Lean users, who wanted a Vim-like experience had to add Vim keybindings to one of the two supported editors, VSCode or Emacs, but these weren't close to the real thing.

Improve this answer
$\endgroup$
3
  • 1
    $\begingroup$ Can you maybe extend the answer with a list of things you’d be missing compared to the default (VS Code) experience when using vim? Also, only nvim or also vim8? $\endgroup$
    – Joachim Breitner
    Commented Feb 9, 2022 at 9:00
  • 1
    $\begingroup$ @JoachimBreitner done! I actually can't think of too many genuinely missing features, but suggestions to improve the answer are welcome of course $\endgroup$
    – Alex J Best
    Commented Feb 15, 2022 at 21:59
  • $\begingroup$ Cool, maybe I should give it a try. I am a gvim user though, and I detest to have to define my own keybindings (I am entitled in that way and expect good defaults from my tools, even from highly configurable tools) :-) $\endgroup$
    – Joachim Breitner
    Commented Feb 16, 2022 at 13:51
9
$\begingroup$

Coq has the Coqtail plugin for vim and neovim. It doesn't have all the bells and whistles of Proof General but the classic 3-pane UI is all I really need to be productive.

Improve this answer
$\endgroup$
2
$\begingroup$

HOL4 has vim support: see some documentation at the GitHub page. It's true that as of 2022 the emacs mode has had more development, but there are ardent vim users in the HOL community so the vim code is exercised.

Improve this answer
$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.