git.iko.soy/Idris-dev
on 413edee help sign in
Idris-dev/tutorial/starting.tex
158 lines 5.3 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 GNU multiprecision arithmetic library, GMP, available from MacPorts and
12all major Linux distributions.
13\end{itemize}
15\subsection{Downloading and Installing}
17The easiest way to install \Idris{}, if you have all of the prerequisites, is to type:
19\begin{SaveVerbatim}{install}
21cabal update; cabal install idris
23\end{SaveVerbatim}
24\useverb{install}
26\noindent
27This will install the latest version released on Hackage, along with any dependencies.
28If, however, you would like the most up
29to date development version, you can find it on GitHub at
30\url{https://github.com/edwinb/Idris-dev}.
32To check that installation has succeeded, and to write your first \Idris{}
33program, create a file called ``\texttt{hello.idr}'' containing the following
34text:
36\begin{SaveVerbatim}{hello}
38module Main
40main : IO ()
41main = putStrLn "Hello world"
43\end{SaveVerbatim}
44\useverb{hello}
46\noindent
47If you are familiar with Haskell, it should be fairly clear what the program is doing
48and how it works, but if not, we will explain the details later.
49You can compile the program to an executable by entering \texttt{idris hello.idr -o hello}
50at the shell prompt. This will create an executable called \texttt{hello}, which you can run:
52\begin{SaveVerbatim}{hello}
54$ idris hello.idr -o hello
55$ ./hello
56Hello world
58\end{SaveVerbatim}
59\useverb{hello}
61\noindent
62Note that the \texttt{\$} indicates the shell prompt! Some useful options to the
63\texttt{idris} command are:
65\begin{itemize}
66\item \texttt{-o prog} to compile to an executable called \texttt{prog}.
67\item \texttt{--check} type check the file and its dependencies without starting the
68interactive environment.
69\item \texttt{--help} display usage summary and command line options
70\end{itemize}
72\subsection{The interactive environment}
74Entering \texttt{idris} at the shell prompt starts up the interactive
75environment. You should see something like the following:
77\begin{SaveVerbatim}[commandchars=^\{\}]{prompt1}
79$ idris
80 ____ __ _
81 / _/___/ /____(_)____
82 / // __ / ___/ / ___/ Version ^version{}
83 _/ // /_/ / / / (__ ) http://www.idris-lang.org/
84 /___/\__,_/_/ /_/____/ Type :? for help
86Idris>
88\end{SaveVerbatim}
89%$
91\useverb{prompt1}
93\noindent
94This gives a \texttt{ghci}-style interface which allows evaluation of expressions,
95as well as type checking expressions, theorem proving, compilation, editing
96and various other operations. \texttt{:?} gives a list of supported commands,
97as shown in Figure \ref{cmds}. Figure \ref{run1} shows an example run in which
98\texttt{hello.idr} is loaded, the type of \texttt{main} is checked and then
99the program is compiled to the executable \texttt{hello}.
101\begin{SaveVerbatim}[commandchars=\\\{\}]{cmds}
102Idris version \version{}
103-------------------
105 Command Arguments Purpose
107 <expr> Evaluate an expression
108 :t <expr> Check the type of an expression
109 :miss :missing <name> Show missing clauses
110 :i :info <name> Display information about a type class
111 :total <name> Check the totality of a name
112 :r :reload Reload current file
113 :l :load <filename> Load a new file
114 :m :module <module> Import an extra module
115 :e :edit Edit current file using $EDITOR or $VISUAL
116 :m :metavars Show remaining proof obligations (metavariables)
117 :p :prove <name> Prove a metavariable
118 :a :addproof <name> Add proof to source file
119 :rmproof <name> Remove proof from proof stack
120 :showproof <name> Show proof
121 :proofs Show available proofs
122 :c :compile <filename> Compile to an executable <filename>
123 :exec :execute Compile to an executable and run
124 :? :h :help Display this help text
125 :set <option> Set an option (errorcontext, showimplicits)
126 :unset <option> Unset an option
127 :q :quit Exit the Idris system
128\end{SaveVerbatim}
129\codefigs{cmds}{Interactive environment commands}
132\begin{SaveVerbatim}[commandchars=^\{\}]{run1}
134$ idris hello.idr
135 ____ __ _
136 / _/___/ /____(_)____
137 / // __ / ___/ / ___/ Version ^version{}
138 _/ // /_/ / / / (__ ) http://www.idris-lang.org/
139 /___/\__,_/_/ /_/____/ Type :? for help
141Type checking ./hello.idr
142*hello> :t main
143main : IO ()
144*hello> :c hello
145*hello> :q
146Bye bye
147$ ./hello
148Hello world
150\end{SaveVerbatim}
152\codefig{run1}{Sample interactive run}
154\noindent
155Type checking a file, if successful, creates a bytecode version of the file (in
156this case \texttt{hello.ibc}) to speed up loading in future. The bytecode is
157regenerated if the source file changes.