Blodwen adaptation

[cfhammill]

Hi All,

I'm interested in playing with blodwen. Anyone have any suggestions for what needs to be modified to get idris-mode compatible with idris2?

Thanks!

Chris

[david-christiansen]

According to Edwin, the protocol is mostly the same. There seems to be a few new commands, described in the Blodwen repository. I would imagine that pointing the Idris executable at Blodwen would be enough to get most working, and then the new features would be a matter of first adding a buffer local variable stating the protocol version, and then make a few commands send the extra parameters conditional on the version.

[cfhammill]

Thanks so much,

So I tried pointing idris-mode at the blodwen executable:

(setq idris-interpreter-path "blodwen")

but I get Buffer *idris-repl* has no process.

From the Messages buffer:

Idris disconnected: exited abnormally with code 1
idris-send: Buffer *idris-repl* has no process
Making completion list...
Warning from Idris: Uncaught error: INTERNAL ERROR: build/--ide-mode-socket.ttc: File Not Found

Idris disconnected: exited abnormally with code 1

Not sure where to go from here.

[gyroninja]

I'd like support for Blodwen too.

Not sure where to go from here.

I'd like to point out that Blodwen does not support the --ide-mode-socket flag yet. It only supports --ide-mode right now. Right now this package tries to use the protocol over tcp: https://github.com/idris-hackers/idris-mode/blob/master/inferior-idris.el#L134. Normal --ide-mode which Blodwen does support is pretty much the same thing but it is done througth stdin and stdout it appears. Getting this package to handle --ide-mode or porting --ide-mode-socket to Blodwen would be the next step of getting Blodwen support at least functioning. In the furure the enhancements of v2 should be added. Also remember that Blodwen uses a build folder with two metadata files for each file it builds instead of just one (the ibc file). idris-mode offers a way for deleting IBC files, so this should be extended to handle the .ttc and .ttm files. This should just be changed to delete metadata for the file in general. The actual language itself is still called Idris AFAIK, so I don't think much of the user facing interface needs to change. You'll want to add support for recognizing .blod files instead of .idr and you'll want to separate the histories of Idris and Blodwen.

[david-christiansen]

Good points.

It wouldn't be particularly hard to let idris-mode use the stdio interface. It used to do that back in the old days, after all! But side effects in C libraries makes this pretty inconvenient in the long run, so it seems better to get the socket version up and running in Blodwen. That took about 3 hours for the Haskell implementation, and Idris 1 has reasonable socket support, so I don't expect it'd be much more.

WRT deleting IBCs, idris-mode does this to force type checking to happen even when the IBC is newer. This works around an issue where cached data would be loaded, and certain effects (like code highlighting and warnings) would not occur. If Blodwen doesn't have these issues, then there's no reason to delete the intermediate build products.

Also, for Blodwen, we probably need to add another category of compiler metadata for the highlighting code: the quantity annotations on binding forms. Those should give appropriate explanatory tooltips.

[cfhammill]

Thanks @gyroninja and @david-christiansen.

Sounds like there is at least a clear first step. Get socket mode up and running for blodwen. I'll submit a small PR to add this as an open issue on ide-notes for blodwen. Then if I get a chance I can look in to porting the socket mode. Given the back compatibility, fingers crossed it will be a simple port.

[kevinboulain]

For the record, Idris 2 supports --ide-mode-socket flag so you can set idris-interpreter-path. Once https://github.com/edwinb/Idris2/pull/53 is in, idris-mode will have to either strip a bunch of commands or port them to Idris 2.

From a quick test:

• :version doesn't exist (fixable by commenting out idris-repl-insert-banner in idris-repl-update-banner)
• :cd doesn't exist
• :interpret returns :ok "Done", replacing printResult "Done" with pure () seems to unbreak stuff a little
• no :highlight-source after :load-file seems to also break stuff

Now I'm stuck with some evaluation problems in idris-dispatch-event. So there is a little bit of work ahead :)

[bigos]

Has anybody done some work towards Idris2 integration? What needs changing? To keep backwards compatibility with old Idris we need something better than idris-interpreter-path. Do you have any suggestions?

[bigos]

https://github.com/bigos/idris-mode/blob/36db9f91db0e17473324b4362dcb2e00a7ac9dfe/idris-core.el#L35 with example like this where do I start in adopting existing mode to Idris 2?

[abailly]

Hi Jacek,

Current idris-mode works with Idris2, at least for basic cases: Loading file, interacting in REPL, some commands like case split, with introduction, hole extraction, basic syntax highlighting (offsets are wrong with off-by-one errors and it does not highlight types, constructors...). It seems to me that rn most work needs to be done on the Idris2 side to implement missing commands and improve syntax highlighting.

Regards,

Arnaud Bailly - @dr_c0d3

On Sat, Aug 1, 2020 at 3:53 AM Jacek Podkanski [email protected] wrote:

https://github.com/bigos/idris-mode/blob/36db9f91db0e17473324b4362dcb2e00a7ac9dfe/idris-core.el#L35 with example like this where do I start in adopting existing mode to Idris 2?

— You are receiving this because you are subscribed to this thread. Reply to this email directly, view it on GitHub https://github.com/idris-hackers/idris-mode/issues/489#issuecomment-667450289, or unsubscribe https://github.com/notifications/unsubscribe-auth/AAAJ2HKEFJJOFRMQSQR7JIDR6NYTFANCNFSM4GMS377A .

[bigos]

In such case I will wait.

By the way, do you think my description of reloading mode code may be useful?

https://github.com/bigos/idris-mode/blob/wip1/development-notes.org

[abailly]

Hi Jacek, It is for me, useful when hacking on the elisp side. I must admit I am not very proficient at emacs-lisp so I would hardly be able to suggest improvements :)

Arnaud Bailly - @dr_c0d3

On Sat, Aug 1, 2020 at 2:23 PM Jacek Podkanski [email protected] wrote:

In such case I will wait.

By the way, do you think my description of reloading mode code may be useful?

https://github.com/bigos/idris-mode/blob/wip1/development-notes.org http://url

— You are receiving this because you commented. Reply to this email directly, view it on GitHub https://github.com/idris-hackers/idris-mode/issues/489#issuecomment-667523746, or unsubscribe https://github.com/notifications/unsubscribe-auth/AAAJ2HM7HJA6OM6B3Z3YV7TR6QCNNANCNFSM4GMS377A .

[bigos]

@ether42 Did you mean something like that?

https://github.com/bigos/idris-mode/blob/ad1049febb64ffdd8c8d2612bb1d88a5f96b83fd/idris-repl.el#L263