\section{Getting Started}

\subsection{Prerequisites} 

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

\begin{itemize}
\item A fairly recent Haskell platform. Version 2010.1.0.0.1 is currently
sufficiently recent.
\item The Boehm-Demers-Weiser garbage collector library. This is available in
all major Linux distributions, or can be installed from source, available
from \url{http://www.hpl.hp.com/personal/Hans_Boehm/gc/}. Installing from
source is painless on MacOS.
\item The GNU multiprecision arithmetic library, GMP, available from MacPorts and
all major Linux distributions.
\end{itemize}

\subsection{Downloading and Installing}

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

\begin{SaveVerbatim}{install}

cabal update; cabal install idris

\end{SaveVerbatim}
\useverb{install}

\noindent
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 on GitHub at
\url{https://github.com/edwinb/Idris-dev}.

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

\begin{SaveVerbatim}{hello}

module main

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

\end{SaveVerbatim}
\useverb{hello}

\noindent
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 \texttt{idris hello.idr -o hello}
at the shell prompt. This will create an executable called \texttt{hello}, which you can run:

\begin{SaveVerbatim}{hello}

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

\end{SaveVerbatim}
\useverb{hello}

\noindent
Note that the \texttt{\$} indicates the shell prompt! Some useful options to the
\texttt{idris} command are:

\begin{itemize}
\item \texttt{-o prog} to compile to an executable called \texttt{prog}.
\item \texttt{--check} type check the file and its dependencies without starting the 
interactive environment.
\end{itemize}

\subsection{The interactive environment}

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

\begin{SaveVerbatim}{prompt1}

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

Idris>

\end{SaveVerbatim}
%$

\useverb{prompt1}

\noindent
This gives a \texttt{ghci}-style interface which allows evaluation of expressions,
as well as type checking expressions, theorem proving, compilation, editing
and various other operations. \texttt{:?} gives a list of supported commands,
as shown in Figure \ref{cmds}. Figure \ref{run1} shows an example run in which
\texttt{hello.idr} is loaded, the type of \texttt{main} is checked and then
the program is compiled to the executable \texttt{hello}.

\begin{SaveVerbatim}{cmds}
Idris version 0.9.2
-------------------

   Command         Arguments   Purpose
                               
   <expr>                      Evaluate an expression
   :t              <expr>      Check the type of an expression
   :total          <name>      Check the totality of a name
   :r :reload                  Reload current file
   :e :edit                    Edit current file using $EDITOR or $VISUAL
   :m :metavars                Show remaining proof obligations (metavariables)
   :p :prove       <name>      Prove a metavariable
   :a :addproof                Add last proof to source file
   :c :compile     <filename>  Compile to an executable <filename>
   :exec :execute              Compile to an executable and run
   :? :h :help                 Display this help text
   :q :quit                    Exit the Idris system
\end{SaveVerbatim}
\codefigs{cmds}{Interactive environment commands}


\begin{SaveVerbatim}{run1}

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

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

\end{SaveVerbatim}

\codefig{run1}{Sample interactive run}

\noindent
Type checking a file, if successful, creates a bytecode version of the file (in this
case \texttt{hello.ibc}) to speed up loading in future. The bytecode is regenerated if
the source file changes.