Using the arrow keys in the REPL should cycle through recently used commands

[edwinb]

Issue by malte-v
Saturday Apr 18, 2020 at 07:29 GMT
Originally opened as edwinb/Idris2-boot#297

---

Currently using the arrow keys just prints ANSI sequences, which is different from the Idris 1 REPL.

Steps to Reproduce

Enter the Idris 2 REPL and use the arrow keys.

Expected Behavior

It cycles through the recently used commands.

Observed Behavior

Escape sequences get printed.

[edwinb]

Comment by gallais
Saturday Apr 18, 2020 at 08:54 GMT

---

Note that you can use rlwrap to cope with the current limitations

[edwinb]

Comment by edwinb
Tuesday Apr 21, 2020 at 10:29 GMT

---

Yes, I run through rlwrap (in fact I've aliased idris2). This is a fairly big feature request, in practice, requiring readline support or similar, and then leads to wanting tab completion of function names. I actually wonder if a better way is to write a separate fancy REPL via the IDE protocol, and to keep what Idris 2 itself does as simple as possible.

[madushan1000]

Since idris2 is run as a script to chezscheme, is there no way to use chezscheme repl for autocomplete and stuff?

[SmiVan]

Both Idris 1's REPL and Haskell's GHCi rely on haskeline for command-line interface, which in turn relies on haskell's POSIX and Win32 bindings.

In the past, GHCi used to rely on editline, which is a set of bindings to libedit.

---

Alternatively, ChezScheme's REPL "cafe" appears to be using scheme's native read and working just fine, with history and arrows working, so perhaps that could be somehow reused for the idris2 REPL? This would certainly lighten the load from the idris side - leaving it up to the underlying language to deal with the interactive command line.

[michaelmesser]

Is this still wanted given Edwin's comments on #807 (comment)?

Sorry to be a pain, though, but I'd much prefer to do anything at all fancy in the REPL (including readline support) in a separate system, interacting with Idris via the IDE protocol, and keep what we have here using the existing minimal interface. This is partly about keeping dependencies down, and partly about keeping the maintenance burden down.

[ska80]

Can this issue be closed?

[gallais]

Yes. Official recommendation is to either:

• use rlwrap
• implement a standalone fancy REPL (:D)

[Qumeric]

@gallais I don't mind rlwrap solution but I am not sure if everyone is aware of it. Perhaps it shall be added to FAQ or readme?