Getting Started¶

Prerequisites¶

Before installing Idris, you will need to make sure you have all of the necessary libraries and tools. You will need:

A fairly recent Haskell platform. Version 2013.2.0.0 should be sufficiently recent, though it is better to be completely up to date.
The GNU Multiple Precision Arithmetic Library (GMP) is available from MacPorts/Homebrew and all major Linux distributions.

Downloading and Installing¶

The easiest way to install Idris, if you have all of the prerequisites, is to type:

cabal update; cabal install idris

This will install the latest version released on Hackage, along with any dependencies. If, however, you would like the most up to date development version you can find it, as well as build instructions, on GitHub at: https://github.com/idris-lang/Idris-dev.

If you haven’t previously installed anything using Cabal, then Idris may not be on your path. Should the Idris executable not be found please ensure that you have added ~/.cabal/bin to your $PATH environment variable. Mac OS X users may find they need to add ~/Library/Haskell/bin instead, and Windows users will typically find that Cabal installs programs in %HOME%\AppData\Roaming\cabal\bin.

To check that installation has succeeded, and to write your first Idris program, create a file called hello.idr containing the following text:

module Main

main : IO ()
main = putStrLn "Hello world"

If you are familiar with Haskell, it should be fairly clear what the program is doing and how it works, but if not, we will explain the details later. You can compile the program to an executable by entering idris hello.idr -o hello at the shell prompt. This will create an executable called hello, which you can run:

$ idris hello.idr -o hello
$ ./hello
Hello world

Please note that the dollar sign $ indicates the shell prompt! Some useful options to the Idris command are:

-o prog to compile to an executable called prog.
--check type check the file and its dependencies without starting the interactive environment.
--help display usage summary and command line options.

The Interactive Environment¶

Entering idris at the shell prompt starts up the interactive environment. You should see something like the following:

$ idris
    ____    __     _
   /  _/___/ /____(_)____
   / // __  / ___/ / ___/     Version 0.9.17
 _/ // /_/ / /  / (__  )      http://www.idris-lang.org/
/___/\__,_/_/  /_/____/       Type :? for help

Idris>

This gives a ghci style interface which allows evaluation of, as well as type checking of, expressions; theorem proving, compilation; editing; and various other operations. The command :? gives a list of supported commands. Below, we see an example run in which hello.idr is loaded, the type of main is checked and then the program is compiled to the executable hello. Type checking a file, if successful, creates a bytecode version of the file (in this case hello.ibc) to speed up loading in future. The bytecode is regenerated if the source file changes.

$ idris hello.idr
     ____    __     _
    /  _/___/ /____(_)____
    / // __  / ___/ / ___/     Version 0.9.17
  _/ // /_/ / /  / (__  )      http://www.idris-lang.org/
 /___/\__,_/_/  /_/____/       Type :? for help

Type checking ./hello.idr
*hello> :t main
Main.main : IO ()
*hello> :c hello
*hello> :q
Bye bye
$ ./hello
Hello world