# edwinb/Idris-dev forked from idris-lang/Idris-dev

Fetching contributors…
Cannot retrieve contributors at this time
153 lines (113 sloc) 4.79 KB
 \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 Evaluate an expression :t Check the type of an expression :total 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 Prove a metavariable :a :addproof Add last proof to source file :c :compile Compile to an executable :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.