Re: Proof General for Vim

Ah yes sorry for not clarifying that earlier.

My solution so far has been to use CoqIDE and just suck it up, I'll post here if I come up with something workable in Vim

On Thu, Jan 17, 2013 at 8:35 PM, Chris Schneider <chris@christopher-schneider.com> wrote:

I googled up Proof General (an Emacs extension to integrate with Coq, a Formal Proof programming language).  

I know almost nothing about the Coq landscape, but generally Vim's approach to plugins is different than Emacs'.  Vim tends to shell out, and then display the info when it comes back (see something like tpope's Fugitive library as an example).  The other option which is totally viable is the tmux integration approach, where you keep a REPL of some sort in one tmux window, and vim uses tmux's built-ins to write text to that other window.

Anyway, the tl;dr here is that I have no idea.  But maybe you can write just enough for yourself to keep your work moving forward, and evolve from there? (assuming nobody jumps in with a pre-written solution).

- Chris

On Thu, Jan 17, 2013 at 6:25 PM, Tim Chase <vim@tim.thechases.com> wrote:

On 01/16/13 20:14, Danny Gratzer wrote:

I'm starting to work with Coq and I'd prefer I can't seem to find
any tools for Vim like Proof General for interacting with Coq.
Are there any such tools out there?

Having not seen any replies, it might help to detail what "Coq" and "Proof General" are (germane URLs or a description of your desired tools would be useful).  While folks may not know Coq/PG, there may be other similar programs/tools that could be modified to fit your needs.

-tim

--
You received this message from the "vim_use" maillist.
Do not top-post! Type your reply below the text you are replying to.
For more information, visit http://www.vim.org/maillist.php

--
Danny Gratzer

--
You received this message from the "vim_use" maillist.
Do not top-post! Type your reply below the text you are replying to.
For more information, visit http://www.vim.org/maillist.php