Loading ...
Sorry, an error occurred while loading the content.

Re: Proof General for Vim

Expand Messages
  • Tim Chase
    ... 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
    Message 1 of 5 , Jan 17, 2013
    • 0 Attachment
      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
    • Chris Schneider
      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
      Message 2 of 5 , Jan 17, 2013
      • 0 Attachment
        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@...> 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

        --
        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
        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
        Message 3 of 5 , Jan 17, 2013
        • 0 Attachment
          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@...> 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@...> 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
        • Jeroen Budts
          ... Hash: SHA256 ... Did you have a look at the plugins section on vim.org? There are 3 plugins related to coq
          Message 4 of 5 , Jan 18, 2013
          • 0 Attachment
            -----BEGIN PGP SIGNED MESSAGE-----
            Hash: SHA256

            On 01/18/2013 04:14 AM, Danny Gratzer wrote:
            > 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

            Did you have a look at the plugins section on vim.org? There are 3
            plugins related to 'coq'
            (http://www.vim.org/scripts/script_search_results.php?keywords=coq&script_type=&order_by=rating&direction=descending&search=search),
            including one which seems to emulate Coq IDE.

            Jeroen


            -----BEGIN PGP SIGNATURE-----
            Version: GnuPG v2.0.17 (GNU/Linux)

            iQIcBAEBCAAGBQJQ+RIVAAoJEBrqc/v4ufiMcZoQALjShKj9iPwgEcVX8wBb1Q6R
            /YdA1ZM29YLIbWCYQZ6/eO5pjmO2hdOhCYMxZmYlpoCy+3REGgpawlcBrrdsOqI8
            BseoQ/OhzVvuIr0T/7XxNEJDV5XEK0JkUNQgYb8x1RqeVAdM6O4HFbhkqXWCK1ri
            6sRD7ey5iVAHWdbEbRNPoWkaqvW6mh52RLY4AySrt9E7VUj0/PcWIHLq1B15dE0a
            klQ3Qk8Nleqlhr0o4kCkDBl8oOqJcY9dZfMDuyO3hhy4JP0E6IhngFhDeWOAiaBM
            C4meTwWo3UdVeS+RL9DM3ZDTuWiQPaNLt/3VD1jr90HWeAuSioajQZ0kbvhJbm5h
            DR7rREXkeVW3oafCmQCWULKjpQ5ZQyWA04EagzxobVl7E61q9jKlo9DwHqQCfdLS
            wo/D32WfS2lkQ4pUiO8BgFpBBQxi9dR39MuykMjn4wBE348kpFyhpE3f5JKTmKfw
            IMuQDTxUMAnJ1cfMh0DH9BRoX4bH3NcY0Py4ewPScnoYpH7E9sjkjQR94Ecbzdpq
            lVaaBQIDw4Znkk8KmOV3MwZdmWWdNVQkfTtD8rFUwuM7FTj2SMR9YkTtjsACvYaj
            V2jvfa7Wv6JIWhGM4TyZeKsj3SoYk7GinT01vk7OmlI3WwoKaIwTYQQt/ZJXpvo7
            k4j5HMFHt99PiEXvCMBM
            =URsj
            -----END PGP SIGNATURE-----

            --
            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
          Your message has been successfully submitted and would be delivered to recipients shortly.