meraymond2/idris-ide-client

Add Clause can fail in Idris2

meraymond2 opened this issue · 3 comments

meraymond2 commented

The current parsing for the AddClauseReply was done for Idris 1 where that command can never fail. If it didn't work, it would just return an empty string. But in Idris 2, it will return an error.

<< 000018((:add-clause 5 "f") 5)
>> (:return (:error "f not defined here") 5)

I need to fix the parsing, so editors can know not to insert the string if it has failed.

ruippeixotog commented

Thanks for opening this! To be clear, I have Idris 1.3.3 installed and not Idris 2, but I still saw the problem in #24. Does the language server use a different Idris version?

meraymond2 commented

Does the language server use a different Idris version?

No, there's not actually a language server, it just starts the Idris compile in IDE-mode, which exposes similar functionality to an LSP. So it's using whichever version you have on your path.

I had mistakenly assumed you were on Idris 2 because I never came across that response while testing with Idris 1, but it's probably just a case I hadn't personally seen.

  • 👍1
meraymond2 commented

This is fixed in 0.1.4.