Dear all;
## Idris Mode and Idris2
The current Idris Mode for emacs [1] has been somewhat working with
Idris2. Out of the box loading, case-splitting, and insertion of
with-patterns was working, the rest was not. It was my understanding
that the issues were related to Idris2's implementation of the IDE
Protocol i.e. off-by-one errors and not supporting all the features
offered. I was having to swap between the REPL and emacs to get more
interactive features.
## Idris2 no longer works with Idris Mode
It appears (AFAICT) that a recent update to Idris2 has finally stopped
Idris' existing emacs-mode [1] (hosted on Idris-Hackers) working with
Idris2 [2]. When I try to load a file I get an error relating to
applying `cd`. Thus making my experience with Idris2 using emacs
untenable.
## Are others seeing the same issues?
I am wondering how the other (half dozen) users of Idris2 and emacs
are doing? Or am I in the small minority who doesn't use the
idris2-vim mode---hosted on [4]. I am aware of the nascent Idris2 mode
[3] that is hosted on Idris-Community [4]. I have not, however, used
it.
Having the two organisations is a point for a future email.
## What should we do here?
Regardless, my main concern is that the Idris IDE Protocol *should*
allow Idris-mode to work with Idris2 but it is not.
So we can either:
1. abandon Idris-Mode and say it is frozen to work with Idris(1) thus
concentrating efforts on Idris2-mode and Idris2;
2. we invest time in getting Idris2 working with Idris-mode and ensure
that the experience is robust when dealing with Idris1 or Idris2; or
3. wait for the LSP mode to mature then jump ship...
With regards to (2): I do not have the emacs-lisp knowledge, nor the
time, to fix it, but I am happy to shepard those that do.
I am happy to hear thoughts and comments here.
Hopefully we can come to some idea on the way forward.
Thanks
Jan
[1]
https://github.com/idris-hackers/idris-mode
[2]
https://github.com/idris-hackers
[3]
https://github.com/idris-community/idris2-mode
[4]
https://github.com/idris-community