module: add :lang idris2

[ribosomerocker]

Added support for the Idris 2 programming language. This is a new, breaking version of Idris, that isn't supported by the pre-existing module. Idris 1 (the one the pre-existing module supports) is deprecated, but I haven't removed it because some people might still depend on it (no pun intended). I haven't really deprecated the module or anything, I'll be waiting for your input to tell me if you want to do so.

As the Idris 1 language is deprecated and pretty much not at all used at this point, and since the pre-existing module doesn't support Idris 2, this kind of makes the pre-existing module useless for Idris users.

• I searched the issue tracker and this hasn't been PRed before.
• My changes are not on the do-not-PR list for this project.
  (technically not for this, but I have discussed this with the maintainer on Discord and I've been told that it's fine to PR this)
• My commits conform to the git conventions.
• My changes are visual; I've included before and after screenshots.
• I am blindly checking these off.
• Any relevant issues or PRs have been linked to.
  (there are no relevant issues or PRs)
• This a draft PR; I need more time to finish it.

[glyh]

Is there an option for customizing idris's interpreter?

  :custom
  (idris-interpreter-path "idris2"))

[aeonik]

I am a bit confused at the current state of idris2-mode vs idris-mode.

It seems like there was an effort to get idris2-mode merged back into the original idris-mode

You can find some old discussions here:

• Prepare merge gallais/idris2-mode#1
• Merge idris2-mode back into idris-mode idris-hackers/idris-mode#546

Today, I am currently attempting to use Idris2 using Doom's idris-mode, but I had to override the interpreter path: (idris-interpreter-path "idris2"))

• I am able to load Idris2 files into the idris-mode REPL; however, it still feels like there are some broken issues.

I am getting errors when trying to evaluate certain statements from the REPL.

I am very new to Idris, so it's hard for me to decouple my own user errors, and official support.

Here are some errors I am getting

"repl_test.idr" 1L, 6C written
Evaluation returned an error: Error(s) building file repl_test.idr: Couldn't parse declaration.

repl_test:1:1--1:2
 1 | 2 * 4

Company: An error occurred in auto-begin
Company: backend company-capf error "I can't make sense of the completion task:
:browse  (synchronous Idris evaluation failed)" with args (prefix)
funcall: I can't make sense of the completion task:
:browse  (synchronous Idris evaluation failed)

Running Idris2 REPL from the CLI allows me to invoke these statements just fine.

[skykanin]

This assumes you're using lsp-mode. Given that doom emacs supports eglot as well this configuration should conditionally register an lsp client for lsp-mode or eglot depending on which one is enabled.

[ncihnegn]

Seems idris2-mode is abandoned.

[hlissner]

Since idris2-mode is unmaintained, I'll close this. In the meantime, I've added some documentation on how to get some idris2 support in idris-mode. That said, thanks for bringing this to my attention!