git.iko.soy/Idris-dev
on 11dd660 help sign in
Idris-dev/tutorial/starting.tex
152 lines 4.9 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 update; cabal install idris
27\end{SaveVerbatim}
28\useverb{install}
30\noindent
31This will install the latest version released on Hackage, along with any dependencies.
32If, however, you would like the most up
33to date development version, you can find it on GitHub at
34\url{https://github.com/edwinb/Idris-dev}.
36To check that installation has succeeded, and to write your first \Idris{}
37program, create a file called ``\texttt{hello.idr}'' containing the following
38text:
40\begin{SaveVerbatim}{hello}
42module main
44main : IO ()
45main = putStrLn "Hello world"
47\end{SaveVerbatim}
48\useverb{hello}
50\noindent
51If you are familiar with Haskell, it should be fairly clear what the program is doing
52and how it works, but if not, we will explain the details later.
53You can compile the program to an executable by entering \texttt{idris hello.idr -o hello}
54at the shell prompt. This will create an executable called \texttt{hello}, which you can run:
56\begin{SaveVerbatim}{hello}
58$ idris hello.idr -o hello
59$ ./hello
60Hello world
62\end{SaveVerbatim}
63\useverb{hello}
65\noindent
66Note that the \texttt{\$} indicates the shell prompt! Some useful options to the
67\texttt{idris} command are:
69\begin{itemize}
70\item \texttt{-o prog} to compile to an executable called \texttt{prog}.
71\item \texttt{--check} type check the file and its dependencies without starting the
72interactive environment.
73\end{itemize}
75\subsection{The interactive environment}
77Entering \texttt{idris} at the shell prompt starts up the interactive
78environment. You should see something like the following:
80\begin{SaveVerbatim}{prompt1}
82$ idris
83 ____ __ _
84 / _/___/ /____(_)____
85 / // __ / ___/ / ___/ Version 0.9.2
86 _/ // /_/ / / / (__ ) http://www.idris-lang.org/
87 /___/\__,_/_/ /_/____/ Type :? for help
89Idris>
91\end{SaveVerbatim}
92%$
94\useverb{prompt1}
96\noindent
97This gives a \texttt{ghci}-style interface which allows evaluation of expressions,
98as well as type checking expressions, theorem proving, compilation, editing
99and various other operations. \texttt{:?} gives a list of supported commands,
100as shown in Figure \ref{cmds}. Figure \ref{run1} shows an example run in which
101\texttt{hello.idr} is loaded, the type of \texttt{main} is checked and then
102the program is compiled to the executable \texttt{hello}.
104\begin{SaveVerbatim}{cmds}
105Idris version 0.9.2
106-------------------
108 Command Arguments Purpose
110 <expr> Evaluate an expression
111 :t <expr> Check the type of an expression
112 :total <name> Check the totality of a name
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 Compile to an executable 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.2
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}
148\noindent
149Type checking a file, if successful, creates a bytecode version of the file (in this
150case \texttt{hello.ibc}) to speed up loading in future. The bytecode is regenerated if
151the source file changes.