search

idris-hackers / idris-mode

Idris syntax highlighting, compiler-supported editing, interactive REPL and more things for Emacs.
GNU General Public License v3.0
268 stars 70 forks source link

Blodwen adaptation #489

Open cfhammill opened 5 years ago

cfhammill commented 5 years ago

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 commented 5 years ago

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 commented 5 years ago

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 commented 5 years ago

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 commented 5 years ago

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 commented 5 years ago

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 commented 5 years ago

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:

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

bigos commented 4 years ago

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 commented 4 years ago

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 commented 4 years ago

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 notifications@github.com 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 commented 4 years ago

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 commented 4 years ago

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 notifications@github.com 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 commented 4 years ago

@ether42 Did you mean something like that?

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