\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 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.
\item \texttt{--help} display usage summary and command line options
\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.5
  _/ // /_/ / /  / (__  )      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.5
-------------------

   Command         Arguments   Purpose
                               
   <expr>                      Evaluate an expression
   :t              <expr>      Check the type of an expression
   :miss :missing  <name>      Show missing clauses
   :i :info        <name>      Display information about a type class
   :total          <name>      Check the totality of a name
   :r :reload                  Reload current file
   :l :load        <filename>  Load a new file
   :m :module      <module>    Import an extra module
   :e :edit                    Edit current file using $EDITOR or $VISUAL
   :m :metavars                Show remaining proof obligations (metavariables)
   :p :prove       <name>      Prove a metavariable
   :a :addproof    <name>      Add proof to source file
   :rmproof        <name>      Remove proof from proof stack
   :showproof      <name>      Show proof
   :proofs                     Show available proofs
   :c :compile     <filename>  Compile to an executable <filename>
   :exec :execute              Compile to an executable and run
   :? :h :help                 Display this help text
   :set            <option>    Set an option (errorcontext, showimplicits)
   :unset          <option>    Unset an option
   :q :quit                    Exit the Idris system
\end{SaveVerbatim}
\codefigs{cmds}{Interactive environment commands}


\begin{SaveVerbatim}{run1}

$ idris hello.idr
     ____    __     _                                          
    /  _/___/ /____(_)____                                     
    / // __  / ___/ / ___/     Version 0.9.5
  _/ // /_/ / /  / (__  )      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.