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.
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.
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.
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.
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: