Configuration file for REPL

[scarf005]

• [x] I have read CONTRIBUTING.md.
• [x] I have checked that there is no existing PR/issue about my proposal.

Summary

Provide configuration file format idris2.conf like .ghci, which will make it easier to configure REPL in various environment.

Motivation

As discussed in discord, it would be convenient to configure REPL without manually setting up by hand.

The proposal

Follow the way .ghci works where possible.

Loading

unless --no-config is given to idris2 executable, load configuration files in following order:

1. idris2appdata/idris2/idris2.conf, where idris2appdata is $XDG_CONFIG_HOME/idris2 or $HOME/.idris2 on UNIX and C:\Users{username}\AppData\Roaming\idris2 on Windows.
2. ./.idris2 (current working directory)

Format

like in Idris1, only allow newline-separated subset of REPL commands.

Examples

:set showtypes

Technical implementation

As I'm not experienced in idris2 development, it's very vague:

1. The REPL should detect OS, Environment variables (XDG_CONFIG_HOME), and current working directory to collect list of configuration files.
2. The REPL should apply contents of configuration files in order, maybe it could just treat it as list of repl command to simplify implementation.
3. The REPL should print out which configuration files are loaded after initialization.

Alternatives considered

Config file for REPLs are universal, and Idris1 REPL also had initialization script.

Conclusion

By allowing configuration, we may reduce possible bikeshed on defaults for

[mattpolzin]

Although it could be argued that this feature request isn't "fancy" I would say it falls under the CONTRIBUTING guidelines' "unlikely to be accepted" entry worded as follows:

Fancy REPL features (e.g. readline, history, tab completion). We definitely want this, but it would be better implemented as a separate tool using the Idris 2 API, to minimise the maintenance burden on the compiler.

That is, this is one of many good reasons to build a community maintained REPL using the compiler library.