Installing Idris

In this course we will be using the programming language Idris, language version 2. Unless the package manager for your system lets you install a binary (version 0.6 or higher) of idris2, you will need to build it from source. In addition to a standard build environment (git, bash, make, etc.) you will need two things:

Building libGMP itself requires the GNU C compiler, or something that can emulate it like LLVM. Ideally, your package manager could provide you with a precompiled version.

Below are some notes collected from the course staff and students to help you get idris2 installed on your system.

Linux

The package manager for most Linux systems should be able to install binaries for both libGMP and Chez Scheme for you. One potential difficulty is that mainline Chez Scheme does not yet support ARM64 (see this issue). If this is your architecture then you should use the Racket fork of Chez Scheme instead. Note that by default the mainline executable is called chez while the Racket version is called scheme.

Once you have installed both libGMP and Chez Scheme you can install Idris either using your package manager or by following the build instructions in the INSTALL file of the GitHub repo for Idris2.

MacOS

The easiest way to get the dependencies for Idris is to use the HomeBrew package manager. On Intel hardware you can simply run brew install gmp and brew install chezscheme, followed by brew install idris2.

For MacOS on ARM64, you can use HomeBrew to install libGMP, but because mainline Chez Scheme does not yet build on ARM64 you will need to use the Racket fork instead (see above and this issue). Once you have working libGMP and Chez Scheme you can build idris2 following these instructions.

Windows

There are several ways to get a development environment installed on Windows. The easiest is probably to use the Windows Subsystem for Linux (WSL). In this case the installation procedure should be the same as for Linux above.

If instead of WSL you want to build natively for Windows you can use a package manager such as Cygwin to install the necessary dependencies. In this case the course staff will not be able to help you very much because we have limited experience developing on Windows. We encourage Windows users in the course to work together on finding an installation method that works for them.

Editor Integration

Idris can help you write your programs interactively through the use of editor integration. This lets you ask Idris to tell you the type or value of an expression, search documentation, decompose a problem into subproblems, etc. In order to use this feature you will need to use a program editor with a plug-in that supports interactive bidirectional communication with Idris. Currently these include:

Visual Studio Code
idris-vscode
Emacs
idris-mode
Vim
idris-vim