What are we to do about Idris2 and Emacs support?

[Jan de Muijnck-Hughes]

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

[Jan de Muijnck-Hughes]

As a quick addendum, this was raised in relation to:

https://github.com/idris-lang/Idris2/issues/1087

When loading an Idris2 file in Emacs the following error is returned

```

Unrecognised command (next
tokens: [identifier cd, symbol /, identifier home, symbol /, identifier jfdm, symbol /, identifier project, symbol /, identifier border, symbol -]) (synchronous Idris evaluation failed)

```

I am just about to submit an issue for this.

Thanks

Jan

[Jan de Muijnck-Hughes]

Sorry for repeated emails...

I see that there are a few PRs/issues on the GitHub detailing various sub issues.

https://github.com/idris-lang/Idris2/issues?q=is%3Aissue+is%3Aopen+protocol

So good to see some existing work there.

Regardless, the larger issue still stands.

Jan

[Arnaud Bailly]

I have not been using Idris2 a lot recently, so was not bitten by this issue but I agree this is concerning.

Having had more than a cursory look at the idris-mode's code while not being very proficient in emacs lisp, I am concerned about the overall maintainability of this codebase. At least I won't be able to do any significant changes to the code without spending (and wasting) a lot of time understanding it.

Looking at https://github.com/emacs-lsp/lsp-haskell as an example of LSP implementation for Haskell that's currently working and actively developed, it seems much more approachable to go down the LSP route, implementing most stuff in Idris2 and just maintaining a thin adapter in emacs-lisp.

So I would go for 3. while investigating tactical improvements in current idris-mode while "we" wait for lsp-idris2 to come of age.

My 2 cts.

-- 

Arnaud Bailly - @dr_c0d3

--
You received this message because you are subscribed to the Google Groups "Idris Programming Language" group.
To unsubscribe from this group and stop receiving emails from it, send an email to idris-lang+...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/idris-lang/d4473483-ee71-4337-83ac-539faf5a4cb8n%40googlegroups.com.

[Ohad Kammar]

Hi,

If it helps, this patch makes the issue with :cd go away. Like Arnaud, I'm not confident in my elisp fu to send a PR without putting more time into eyeballing it.

Yours,

Ohad.

--- a/idris-commands.el
+++ b/idris-commands.el
@@ -203,7 +203,7 @@ A prefix argument forces loading but only up to the current line."
         ;; Actually do the loading
         (let* ((dir-and-fn (idris-filename-to-load))
                (fn (cdr dir-and-fn))
-               (srcdir (car dir-and-fn)))
+               (srcdir (prin1-to-string (car dir-and-fn))))
           (setq idris-currently-loaded-buffer nil)
           (idris-switch-working-directory srcdir)
           (idris-delete-ibc t) ;; delete the ibc to avoid interfering with partial loads

[Jan de Muijnck-Hughes]

Thanks for the swift responses so far.

@Arnaud, My main concern with LSP, is that I am not yet sure *if* it
can replicate all of the existing IDE-protocol functionality. I have
yet to read through *that* github issue.

My concern with the Idris compilers, the editor clients, and the IDE
protocol, is that I think we should maintain backwards compatibility,
and if not, evolve the protocol and ensure that the editor clients
work with the protocol and it's versions. The protocol is versioned!

Thus, whilst Ohad's fix looks okay, (and I think a similar fix was
made to the Idris2-mode on idris-community), it doesn't really address
the divergence in the IDE-Protocol, updating it's versioning et
cetera...We will need to update Idris1 as well...

Thanks

Jan

> --
> You received this message because you are subscribed to the Google Groups "Idris Programming Language" group.
> To unsubscribe from this group and stop receiving emails from it, send an email to idris-lang+...@googlegroups.com.

> To view this discussion on the web visit https://groups.google.com/d/msgid/idris-lang/CAGkJaNXsbKQ2_8z7oqpJ0pFsXgbz5EH4%3D%2BD61gj3egim8sTChA%40mail.gmail.com.

[Ohad Kammar]

Hi Jan,

Thanks for this. The main issue with idris-mode is that it's not 'owned' by anyone (in the open-source interpretation).

The versioning in the IDE protocol doesn't help with the basic issue: someone still needs to implement the control-flow in the elisp code, and that someone need to be confident in the current design.

Ohad.

To view this discussion on the web visit https://groups.google.com/d/msgid/idris-lang/CACrPt3TwBv-xmY5c7bUBtM9gbGw-QThrVQ0HqeL7Mw%3DQq6tqZA%40mail.gmail.com.

[Jacek Podkanski]

I would be willing to help in one way or another, depending on what you decide.

In the past, I tried to tinker with my own patches to idris-mode.

[Arnaud Bailly]

On Fri, Feb 19, 2021 at 12:32 PM Jan de Muijnck-Hughes <j.demuij...@gmail.com> wrote:

Thanks for the swift responses so far.

@Arnaud, My main concern with LSP, is that I am not yet sure *if* it
can replicate all of the existing IDE-protocol functionality. I have
yet to read through *that* github issue.

 

I don't think this really a big issue, or should really be a concern if we care about providing a smooth developer experience. 

I am old enough to remember the days of videotapes and the fight between Betamax and VHS: In the end, VHS won although everyone agreed Betamax was technically superior. And it won because more vendors supported it and it was better marketed than its competitor. LSP is becoming the de facto standard in IDE tooling, supported by more and more tools and languages ecosystems, so it does not make much sense to me to not fully embrace it.

YMMV as always

Arnaud

[Jan de Muijnck-Hughes]

Thanks all.

The downside of this discussion is that I have had to learn some more
emacs-lisp :-(

So reading up on the original idris-mode and how the
idris-ide-protocol works (together with some failed improvements and
closed PRs) we *do* have someone able to start making idris-mode
compatible with idris2's protocol changes in a backwards compatible
way: c'est moi....

Ohad is right...someone has to take ownership of Idris-mode and
guide/make changes.

I have made a draft change to the idris-mode that should *hopefully*
demonstrate a potential way forward.

https://github.com/idris-hackers/idris-mode/pull/517

Now there still remains potential issues in that idris2 wasn't
interacting with idris-mode in ways that it should have already.

We have, however, a way to move forward until those issues are resolved.

So if anyone wants to chip in, please do. I am happy to shepherd.

I have already seen some pending PRs that need addressing from last
time I looked at the idris-mode. Apologies for those ignored there...

Thanks

Jan

> --
> You received this message because you are subscribed to the Google Groups "Idris Programming Language" group.
> To unsubscribe from this group and stop receiving emails from it, send an email to idris-lang+...@googlegroups.com.

> To view this discussion on the web visit https://groups.google.com/d/msgid/idris-lang/CAL4zPapZ%2BB85ekrko_z_7c3tX0jfQC_q3qqC7890wCREDdG4fg%40mail.gmail.com.

[nichol...@gmail.com]

I hadn't used Idris for a while, and then when I tried it again last
month it wouldn't work with Emacs. Like not at all. I just now updated
idris-mode to the latest and it works. I don't know if it works
perfectly, but I can confirm that it has gone from "can't use it at
all" to "works well enough". Great job Jan! Jan can cook!

[Ohad Kammar]

Dear Nicholas,

There's a fork mode:

https://github.com/redfish64/idris2-mode

which works OK at the moment.

Yours,

Ohad.

To view this discussion on the web visit https://groups.google.com/d/msgid/idris-lang/5e8ae50c-9171-4a34-9478-eb9e89a79f6cn%40googlegroups.com.