Proof search fails with Idris 2

[scotek]

Trying to perform a proof search while connected to Idris 2 always fails with an error, which also hangs Emacs (I'm using GNU Emacs 26.1, Idris 2 from git db9f7bbf on WSL ).

Example input file:

fn : a -> a -> (a,a)
fn x y = ?aaa

bar : a -> b -> b -> b
bar x y z = ?bbb

Move point to somewhere inside the ?aaa hole and attempt to solve hole. The following error appears in the mini-buffer:

error in process filter: Unexpected reply: 10 (:error "Parse error: Parse error: Expected ')' (next tokens: [symbol (, symbol :, identifier proof-search, literal 3, string \"aaa\", identifier nil, symbol ), literal 11, symbol ), end of input])")

(Emacs then hangs with a spinning activity cursor and needs to be killed)

I've tried to go through both idris-mode and Idris 2's IDE mode code but the elisp is too advanced for me to follow properly. I can get proof search working if I remove the hints and depth arguments from the idris-eval call in idris-proof-search. ie, idris-commands.el line 745 becomes:

      (let ((result (car (idris-eval `(:proof-search ,(cdr what) ,(car what))))))

Proof search calls then work as expected in both Idris 2 and Idris 1, but this removes the optional extra functionality when using Idris 1.

[jfdm]

Thanks for the contributions!

I am not sure what is going on here, I am not an emacs lisp expert nor how this ties into ide-protocol...It might be that something has diverged somewhere.

Might be one to bring up on the mailing list.

[jfdm]

fixed in #511