Idris is available from on hackage,
http://hackage.haskell.org/package/idris, via cabal install idris.
Alternatively, you can get the source from
http://www.cs.st-and.ac.uk/~eb/Idris. You can download a package
containing the latest version from http://www-fp.cs.st-and.ac.uk/~eb/idris/idris-current.tgz. To install, you will require GHC 6.10 or greater, and the
Boehm garbage collector. This is available from
http://www.hpl.hp.com/personal/Hans_Boehm/gc/ or as a package from
Macports or your favourite Linux distribution.
Download the package, untar it with tar zxvf idris-current.tgz,
cd to the new directory (which will have a name of the form
idris-date where date gives the date the package was created, then
type make. This will install the idris executable in your home
directory.
Before we start writing programs, let us check whether the
installation has succeeded, and show how to compile and run simple
programs. We will start with the standard 'Hello world'
program. Enter the following text into a file called hello.idr:
main : IO ();main = putStrLn "Hello world"; To run this program, type idris hello.idr at the shell
prompt. If it loads successfully, you will be presented with an Idris
prompt, Idris>. At this prompt, you can give commands to this Idris
system, or expressions to be evaluated. To run the program, type
main. You should see something like the following (where $ stands
for your shell prompt):
$ idris hello.idrIdris> mainHello worldIIIdris> :q$ The program prints Hello world. II is the element of the unit
type, which is the value returned by main - don't worry about this
for now.
As well as evaluating expressions at the Idris prompt, you can execute commands to do various things, such as:
:c <executable>)
:t <expression>)
:o <options>)
:p <theorem>)
:q)
:? or :h)
For example, to get the type of main then compile hello.idr to an executable:
$ idris hello.idrIdris> :t mainIO ()Idris> :c helloIdris> :q$ ./helloHello world$ Finally, it is also possible to compile to an executable from the
shell in 'batch mode', using the -o option:
$ idris hello.idr -o hello$ ./helloHello world$This example, like all of the examples in this tutorial, is generated from an Idris source file. You can find this here.