Setting Up Idris for Development

When I started out with Idris, I didn't find a unified set of instructions on how to get started; instead there were multiple resources spread out across the internet. This is my attempt to write down what I wish I had seen earlier.

I prefer to bootstrap Idris instead of downloading an executable, so to do that we'll need to install chez scheme. On Ubuntu 20.04, it's available from the universe repository:

> sudo apt install chezscheme

For MacOS, I prefer using homebrew:

> brew install chezscheme

On Ubuntu that will place the chezscheme executable into your path, and on MacOS it's chez.

Next is the bootstrapping process, for which I prefer using pack. Due to the name, its discoverability has a bit to be desired, which is why I have it bookmarked for easy access. Follow the instructions in the readme. If you're using a somewhat nonstandard shell (I use fish), you may need to manually add its folder to your path. For example, in my fish config file I have a line similar to

fish_add_path -g ~/.idris2/bin ~/.pack/bin

Next we'll use pack to install the lsp server for use in VSCode:

> pack install-app lsp

Any time you upgrade pack/idris, you'll probably want to rerun this command or else you'll get lsp errors in VSCode. Next is editor integration, for which I prefer idris2-lsp by Rodrigo Bamboo. Now you should be able to use pack to start a new project:

> pack new bin hello-world
> cd hello-world
> code .

Take a look at the generated hello-world.ipkg file, this is where most of the project's config will go. Two of the more important fields here are depends and opts. If you wanted to depend on the contrib library and compile to node, for example, you'd have:

depends = contrib
opts = "--cg node"

then build it with pack build hello-world.ipkg. Idris also has a useful REPL (at least, more useful than PureScript's psci), and you can enter it via

> pack --with-ipkg hello-world.ipkg repl src/Main.idr

Finally, idris lsp integration is different from PureScript, for example. In PS, if you wanted to generate a clause given a type signature, you'd set the cursor over the type and use the Command Palette to tell VSCode what to do. With idris, almost everything is a code action: you place your cursor over the type and press ctrl + . (cmd + . in MacOS), then select "Add clause". I'll admit, when I was getting started I thought maybe there was no lsp functionality built in to the VSCode extension for idris, since searching the Command Palette for "idris" gave such a small set of results.