Completion incompatible with running interactive programs in REPL

[david-christiansen]

I'm currently working on a program that has a REPL-like interaction built in. When I run this in the racket-mode REPL, I can interact with it just fine. However, it seems that whenever Racket attempts to complete the symbol at point, it enters garbage data into my program behind the scenes. It would seem that there's some in-band communication going on. This means that, in practice, company-mode makes the racket-mode REPL unsuitable for testing text-mode interactive programs.

It seems to me that there's two reasonable ways to fix this:

1. Move communication about completion, etc. out-of-band, e.g. to a socket
2. Provide a way to run a Racket program with it's I/O ports redirected to a separate comint buffer, so they don't interfere with racket-mode's requests to Racket.

[greghendershott]

Thanks for the report. Although not necessarily a common use case, this definitely hits a weak point with the current approach.

I have a now-stale branch where I'd experimented with using a socket. IIRC I got it to work AFACIT -- but I was nervous about concurrency bugs, and didn't see a compelling benefit then (didn't think of a use case like you're pointing out, now).

I'd love to revive that. However to be realistic I don't think I will have enough time in the very near future to code -- and more importantly, sufficiently test and dogfood -- this sort of change.

[david-christiansen]

A move to a socket made idris-mode much more reliable, in any case.

Fair enough with the lack of time, I think that's a universal affliction :) I think this will be a good motivation for me to get a GUI or an Emacs-based UI together for my proof assistant sooner rather than later!

[greghendershott]

A move to a socket made idris-mode much more reliable, in any case.

If I understand what you mean here, racket-mode has already "half-moved" to the equivalent.

Originally command response output went to stdout, mixed with the user's program's output, and intercepted/extracted by a comint filter function. With < 100% success. That was not very reliable.

Awhile ago I changed to having command responses go into a file. (Well, ,command still displays in the buffer, but #,command redirects to the special file; racket-mode Elisp mostly uses the latter.) That has been a huge help.

AFAICT a socket and a special file are equivalent in terms of the key benefit of separating command response from user program output, thereby avoiding all sorts of bugs trying to un-mix the two.

However that leaves input -- separating command requests from input to the user's program. That's obvious now that you point it out. I think it's been moot because I just haven't written Racket programs that do interactive input (as opposed to server or or GUI programs), and maybe most other racket-mode users so far, too. But I agree it ought to work. And I agree it probably makes sense to use a socket now for both I and O.

I would need to think about the concurrency, and what it would mean for command requests to arrive that way -- as opposed to the status quo of simply being some syntax returned by current-read-interaction as called by read-eval-print-loop on the user's program's main thread. I think of this as being roughly like how you'd prefer to get commands as events on the main thread in a GUI.

[david-christiansen]

Yes, I think the socket and the file are equivalent from a safety perspective. One downside of the socket approach is that it looks like two processes in Emacs, one for the compiler and one for the connection, because we also run the compiler in comint-mode in case the user writes a program that e.g. does IO during type checking.

In idris-mode, we use essentially the same protocol as slime and dime to attach requests to responses. Each request from Emacs comes with an ID number (which Emacs is responsible for maintaining the uniqueness of). Then, responses from Idris all use that ID. When Idris sends the last response to a request, it indicates that it's finished.

In Emacs, then, we have a table mapping request IDs to continuations that will handle responses on them. When a response comes from Idris, it is unpacked by idris-mode and then the payload is sent to the appropriate continuation.

The docs are here: http://docs.idris-lang.org/en/latest/reference/ide-protocol.html

Hope that's handy.

[david-christiansen]

Thanks!

[greghendershott]

You're welcome! It was a fairly big change, so I'm kind of waiting for the other shoe to drop. But I'm glad I did it. Please let me know if anything isn't working as you expected.