idris-send: Buffer *idris-repl* has no process

[mhwombat]

I have been using the REPL in idris-mode just fine. But in the last hour, something broke. Now when I start the REPL (by invoking idris-load-file on a source file), a buffer opens and the Idris logo is displayed, but I don't get a prompt.

The messages buffer has:

idris-send: Buffer *idris-repl* has no process
Connected. Amy, this could be the start of a beautiful proof.
Mark set [3 times]

the idris-process and iddris-connection buffers are empty.

I can start a REPL at the command line just fine.

$ idris
     ____    __     _                                          
    /  _/___/ /____(_)____                                     
    / // __  / ___/ / ___/     Version 1.3.0
  _/ // /_/ / /  / (__  )      http://www.idris-lang.org/      
 /___/\__,_/_/  /_/____/       Type :? for help               

Idris is free software with ABSOLUTELY NO WARRANTY.            
For details type :warranty.
Idris> 

I can only think of two things that changed recently.

1) I made some changes to the key bindings in Emacs, but since the REPL is being invoked, I don't think this is the cause of the problem. 2) I upgraded my NixOS installation, which could also have picked up changes from Melpa. (I'm still on NixOS 18.09, though. Can't use 19.03 because of this issue) Perhaps something changed in how the REPL is launched?

[mhwombat]

OK, this is truly bizarre. It started working again. The only thing I did that might have "fixed" it was that I typed M-x idris-repl instead of using my key binding, which worked. After that, everything (including my key binding) started working again.

[mhwombat]

And now it's stopped working again.

[mhwombat]

It's working intermittently. I've found a pattern and a workaround. The workaround is to try loading a file, again if necessary. If I had to guess, I'd say some part of the code isn't waiting long enough for Idris to respond, so it displays the "idris-send: Buffer idris-repl has no process" message and gives up.

Scenario A Starting the REPL before loading a file.

1. I start emacs.
2. I start a REPL (M-x idris-repl). The repl buffer is created and the Idris logo is displayed. But whether or not I actually get a prompt seems to be random.
3. I load a source file (see helloIdris.idr, below).
4. I load the file in Idris (M-x idris-load-file). a) If I didn't get a prompt in step 1, the Idris logo disappears and I see

   <no Idris logo>
   Type checking ./helloIdris.idr
   λΠ> 

   along with the "No holes found!" status message. b) If I did get a prompt in step 1, the logo does not disappear. I see:

   <Idris logo>
   Type checking ./helloIdris.idr
   λΠ> 

   along with the "No holes found!" status message.

Scenario B Loading a file without starting a REPL first.

1. I start emacs.
2. I load a source file (see helloIdris.idr, below).
3. I load the file in Idris (M-x idris-load-file). The repl buffer is created and the Idris logo is displayed. But whether or not I actually get a prompt seems to be random. a) If I didn't get a prompt in step 3, after waiting 10 seconds I load it again (M-x idris-load-file). The Idris logo disappears and I see:

   <no Idris logo>
   Type checking ./helloIdris.idr
   λΠ> 

   along with the "No holes found!" status message. b) If I did get a prompt in step 3, I'm done.

Here's helloIdris.idr

module Main

import Data.Vect

main : IO ()
main = putStrLn "Hello world"

[mhwombat]

Oops, closed by accident when I posted the workaround.

[mhwombat]

This issue may be related: #458

[jsoo1]

I think this may have more or less to do with not dealing with the asynchronous process perfectly everywhere.