git.iko.soy/Idris-dev
on 11d4fee help sign in
Idris-dev/tutorial/starting.tex
151 lines 5.0 kB history raw
1\section{Getting Started}
3\subsection{Prerequisites}
5Before installing \Idris{}, you will need to make sure you have all of the necessary
6libraries and tools. You will need:
8\begin{itemize}
9\item A fairly recent Haskell platform. Version 2010.1.0.0.1 is currently
10sufficiently recent.
11\item The Boehm-Demers-Weiser garbage collector library. This is available in
12all major Linux distributions, or can be installed from source, available
13from \url{http://www.hpl.hp.com/personal/Hans_Boehm/gc/}. Installing from
14source is painless on MacOS.
15\item The GNU multiprecision arithmetic library, GMP, available from MacPorts and
16all major Linux distributions.
17\end{itemize}
19\subsection{Downloading and Installing}
21The easiest way to install \Idris{}, if you have all of the prerequisites, is to type:
23\begin{SaveVerbatim}{install}
25cabal install idris
27\end{SaveVerbatim}
28\useverb{install}
30\noindent
31This will install the latest version released on Hackage\footnote{However version 0.9, which
32this tutorial describes, is not yet there, so don't do this. Finishing this tutorial is the
33last requirement before releasing it :-).}, along with any dependencies.
34If, however, you would like the most up
35to date development version, you can find it on GitHub at
36\url{https://github.com/edwinb/Idris-dev}.
38To check that installation has succeeded, and to write your first \Idris{}
39program, create a file called ``\texttt{hello.idr}'' containing the following
40text:
42\begin{SaveVerbatim}{hello}
44module main;
46main : IO();
47main = putStrLn "Hello world";
49\end{SaveVerbatim}
50\useverb{hello}
52\noindent
53If you are familiar with Haskell, it should be fairly clear what the program is doing
54and how it works, but if not, we will explain the details later.
55You can compile the program to an executable by entering \texttt{idris hello.idr -o hello}
56at the shell prompt. This will create an executable called \texttt{hello}, which you can run:
58\begin{SaveVerbatim}{hello}
60$ idris hello.idr -o hello
61$ ./hello
62Hello world
64\end{SaveVerbatim}
65\useverb{hello}
67\noindent
68Note that the \texttt{\$} indicates the shell prompt! Some useful options to the
69\texttt{idris} command are:
71\begin{itemize}
72\item \texttt{-o prog} to compile to an executable called \texttt{prog}.
73\item \texttt{--check} type check the file and its dependencies without starting the
74interactive environment.
75\end{itemize}
77\subsection{The interactive environment}
79Entering \texttt{idris} at the shell prompt starts up the interactive
80environment. You should see something like the following:
82\begin{SaveVerbatim}{prompt1}
84$ idris
85 ____ __ _
86 / _/___/ /____(_)____
87 / // __ / ___/ / ___/ Version 0.9
88 _/ // /_/ / / / (__ ) http://www.idris-lang.org/
89 /___/\__,_/_/ /_/____/ Type :? for help
91Idris>
93\end{SaveVerbatim}
94%$
96\useverb{prompt1}
98This gives a \texttt{ghci}-style interface which allows evaluation of expressions,
99as well as type checking expressions, theorem proving, compilation, editing
100and various other operations. \texttt{:?} gives a list of supported commands,
101as shown in Figure \ref{cmds}. Figure \ref{run1} shows an example run in which
102\texttt{hello.idr} is loaded, the type of \texttt{main} is checked and then
103the program is compiled to the executable \texttt{hello}.
105\begin{SaveVerbatim}{cmds}
106Idris version 0.9
107-----------------
109 Command Arguments Purpose
111 <expr> Evaluate an expression
112 :t <expr> Check the type of an expression
113 :r :reload Reload current file
114 :e :edit Edit current file using $EDITOR or $VISUAL
115 :m :metavars Show remaining proof obligations (metavariables)
116 :p :prove <name> Prove a metavariable
117 :a :addproof Add last proof to source file
118 :c :compile <filename> Compile to an executable <filename>
119 :exec :execute <filename> Compile to an executable <filename> and run
120 :? :h :help Display this help text
121 :q :quit Exit the Idris system
122\end{SaveVerbatim}
123\codefigs{cmds}{Interactive environment commands}
126\begin{SaveVerbatim}{run1}
128$ idris hello.idr
129 ____ __ _
130 / _/___/ /____(_)____
131 / // __ / ___/ / ___/ Version 0.9
132 _/ // /_/ / / / (__ ) http://www.idris-lang.org/
133 /___/\__,_/_/ /_/____/ Type :? for help
135Type checking ./hello.idr
136*hello> :t main
137main : IO ()
138*hello> :c hello
139*hello> :q
140Bye bye
141$ ./hello
142Hello world
144\end{SaveVerbatim}
146\codefig{run1}{Sample interactive run}
148Type checking a file, if successful, creates a bytecode version of the file (in this
149case \texttt{hello.ibc}) to speed up loading in future. The bytecode is regenerated if
150the source file changes.