search

edwinb / Idris2-boot

A dependently typed programming language, a successor to Idris
https://idris-lang.org/
Other
902 stars 58 forks source link

#297: Adding support for readline at the REPL #335

Open rgrover opened 4 years ago

rgrover commented 4 years ago

Switching the REPL to use readline instead of getLine. Added Text/Readline for bindings.

Note: the implementation of readline currently doesn't turn the received input into a buffer managed by the runtime system, and hence is quite likely incomplete.

This is a strawman. I'm happy to take this further and turn the REPL into a separate lightweight application as suggested here. I'd need some input for that.

rgrover commented 4 years ago

This adds a dependency on readline. The CI system will need to be updated if this is to go ahead.

FranckS commented 4 years ago

I would definitely love to see the Repl for idris2 become like the one idris1 had. Especially navigating through recently typed commands with the upper and lower keys, and if doable tab suggestions/auto completion. I don't know what's the best way to do that, so this message is just an encouragement, many thanks for your work on this @rgrover !

edwinb commented 4 years ago

We definitely need a nicer REPL, and proper readline support will help there. I just run via rlwrap at the moment. In the end, I think a nicer way to do it is to go via the IDE protocol and to keep what Idris itself does as simple as possible - this is at least partly about giving me less to worry about in the core of Idris itself as really I need to understand what's going on in all parts of the system. Also because it already takes ages to build and more features will make it even worse. Getting to a self hosted state will help here, but that'll still take a little while.

So I think my main worry at the moment is that this doesn't do much more than running via rlwrap and to take it further will slow things down even more for developers. What input would you need for developing a separate REPL application?

The IDE protocol is described at http://docs.idris-lang.org/en/latest/reference/ide-protocol.html Idris 2 doesn't do all of it yet, but it does do the basics. Actually you could test it by writing a nice REPL for Idris 1 which Idris 2 would then support later!