Crash on Coq 8.5

[nilehmann]

The plugin doesnt work anymore in coq 8.5, is there intention to work on this?

[nadimkobeissi]

Bump

[osa1]

👍

I haven't switched to Coq 8.5 yet(it works fine with 8.4pl5), but I'll need this when I switch.

[trefis]

Yes, this is a known problem.
The protocol changed, and there is currently no plan to update coquille to work with 8.5...

Sorry.

[anishathalye]

I'm not familiar with coquille code or the coqtop protocol, so before I think about attempting to fix this to work with 8.5 -- any idea how long it might take?

[Ptival]

What does coquille need from coqtop to work? I have a bit of experience
with the new protocol, you can lookup the PeaCoq/src project directory.
Good luck!

On Sun, Apr 24, 2016, 17:54 Anish Athalye [email protected] wrote:

I'm not familiar with coquille code or the coqtop protocol, so before I
think about attempting to fix this to work with 8.5 -- any idea how long it
might take?

—
You are receiving this because you are subscribed to this thread.
Reply to this email directly or view it on GitHub
#31 (comment)

[anishathalye]

Okay, so the main functionality is in https://github.com/the-lambda-church/coquille/blob/pathogen-bundle/autoload/coquille.py, so we don't need to write any vimscript, which is nice.

The first thing that needs to be fixed is how Coq is launched:

diff --git i/autoload/coquille.py w/autoload/coquille.py
index 1de3a9a..9b4baca 100644
--- i/autoload/coquille.py
+++ w/autoload/coquille.py
@@ -73,14 +73,14 @@ def restart_coq(*args):
     try:
         if os.name == 'nt':
             coqtop = subprocess.Popen(
-                    ["coqtop", "-ideslave"] + list(args),
+                    ["coqtop", "-main-channel", "stdfds", "-ideslave"] + list(args),
                     stdin = subprocess.PIPE,
                     stdout = subprocess.PIPE,
                     stderr = subprocess.STDOUT
                     )
         else:
            coqtop = subprocess.Popen(
-                    ["coqtop", "-ideslave"] + list(args),
+                    ["coqtop", "-main-channel", "stdfds", "-ideslave"] + list(args),
                     stdin = subprocess.PIPE,
                     stdout = subprocess.PIPE,
                     preexec_fn = ignore_sigint

(via http://coq-club.inria.narkive.com/UC4eD9Lg/coqtop-ideslave-on-mac-os-x)

After that, the send_until_fail() function will need to be updated.

Is there any document anywhere that explains how the protocol has changed? Looks like coqtop -toploop coqidetop --help-XML-protocol gives info about the current state of the protocol but doesn't talk about what has changed.

[anishathalye]

A quick update in case anyone is curious:

Looking at the current interface, it looks like some of the things just changed slightly. For example, interp is now Interp, and the RPC takes a couple extra arguments. So those aren't a big deal to fix.

However, it looks like the rewind RPC was removed entirely (even though it's still mentioned in a comment at the top of ide_slave.ml).

rewind was removed in favor of backto in coq/coq@a936e9a, and backto was removed in coq/coq@698a1ca in favor of the new protocol.

So it seems like this would be some effort to fix.

[elfi]

@anishathalye you might want to check neovim-coq scripts (python) - https://github.com/epdtry/neovim-coq . That seems to be updated for coq8.5.

[swr1bm86]

@elfi thx for citing this link and this neovim package seems unfinished but it do provide a reusable coqtop abstraction layer.

@anishathalye you're right, the interp and rewind commands are completely removed from ide slave and since the new protocol uses state machine, we can easily mock this two things with Add and Edit_at commands.