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

Proof General for Vim

Expand Messages
  • Danny Gratzer
    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
    Message 1 of 5 , Jan 16, 2013
    • 0 Attachment
      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?

      --
      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
    • 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 2 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 3 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 4 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 5 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.