git.iko.soy/Idris-dev
on d1663cc help sign in
Idris-dev/tutorial/content/starting.tex
145 lines 5.6 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{lstlisting}[language=bash]
20cabal update; cabal install idris
21\end{lstlisting}
23\noindent
24This will install the latest version released on Hackage, along with any dependencies.
25If, however, you would like the most up
26to date development version, you can find it on GitHub at
27\url{https://github.com/edwinb/Idris-dev}.
29To check that installation has succeeded, and to write your first \Idris{}
30program, create a file called ``\texttt{hello.idr}'' containing the following
31text:
33\begin{code}
34module Main
36main : IO ()
37main = putStrLn "Hello world"
38\end{code}
40\noindent
41If you are familiar with Haskell, it should be fairly clear what the program is doing
42and how it works, but if not, we will explain the details later.
43You can compile the program to an executable by entering \texttt{idris hello.idr -o hello}
44at the shell prompt. This will create an executable called \texttt{hello}, which you can run:
46\begin{lstlisting}[language=bash]
47$ idris hello.idr -o hello
48$ ./hello
49Hello world
50\end{lstlisting}
52\noindent
53Note that the \texttt{\$} indicates the shell prompt! Some useful options to the
54\texttt{idris} command are:
56\begin{itemize}
57\item \texttt{-o prog} to compile to an executable called \texttt{prog}.
58\item \texttt{--check} type check the file and its dependencies without starting the
59interactive environment.
60\item \texttt{--help} display usage summary and command line options
61\end{itemize}
63\subsection{The interactive environment}
65Entering \texttt{idris} at the shell prompt starts up the interactive
66environment. You should see something like the following:
68\begin{lstlisting}[escapechar=^]
69$ idris
70 ____ __ _
71 / _/___/ /____(_)____
72 / // __ / ___/ / ___/ Version ^\version{}^
73 _/ // /_/ / / / (__ ) http://www.idris-lang.org/
74 /___/\__,_/_/ /_/____/ Type :? for help
76Idris>
77\end{lstlisting}
79\noindent
80This gives a \texttt{ghci}-style interface which allows evaluation of expressions,
81as well as type checking expressions, theorem proving, compilation, editing
82and various other operations. \texttt{:?} gives a list of supported commands,
83as shown in Figure \ref{cmds}. Figure \ref{run1} shows an example run in which
84\texttt{hello.idr} is loaded, the type of \texttt{main} is checked and then
85the program is compiled to the executable \texttt{hello}.
87\begin{lstlisting}[caption={Interactive environment commands}, label=cmds, escapechar=^]
88Idris version ^\version{}^
89--------------------
91 Command Arguments Purpose
93 <expr> Evaluate an expression
94 :t <expr> Check the type of an expression
95 :miss :missing <name> Show missing clauses
96 :i :info <name> Display information about a type class
97 :total <name> Check the totality of a name
98 :r :reload Reload current file
99 :l :load <filename> Load a new file
100 :cd <filename> Change working directory
101 :m :module <module> Import an extra module
102 :e :edit Edit current file using $EDITOR or $VISUAL
103 :m :metavars <metavar> Show remaining proof obligations (metavariables)
104 :p :prove <metavar> Prove a metavariable
105 :a :addproof <name> Add proof to source file
106 :rmproof <name> Remove proof from proof stack
107 :showproof <name> Show proof
108 :proofs Show available proofs
109 :x <expr> Execute IO actions resulting from an expression
110 using the interpreter
111 :c :compile <filename> Compile to an executable <filename>
112 :js :javascript <filename> Compile to JavaScript <filename>
113 :exec :execute Compile to an executable and run
114 :dynamic <filename> Dynamically load a C library (similar to %dynamic)
115 :dynamic List dynamically loaded C libraries
116 :? :h :help Display this help text
117 :set <option> Set an option (errorcontext, showimplicits)
118 :unset <option> Unset an option
119 :colour :color <option> Turn REPL colours on or off; set a specific colour
120 :q :quit Exit the Idris system
121\end{lstlisting}
123\begin{lstlisting}[caption={Sample Interactive Run}, label=run1, escapechar=^]
124$ idris hello.idr
125 ____ __ _
126 / _/___/ /____(_)____
127 / // __ / ___/ / ___/ Version ^\version{}^
128 _/ // /_/ / / / (__ ) http://www.idris-lang.org/
129 /___/\__,_/_/ /_/____/ Type :? for help
131Type checking ./hello.idr
132*hello> :t main
133main : IO ()
134*hello> :c hello
135*hello> :q
136Bye bye
137$ ./hello
138Hello world
139\end{lstlisting}
141\noindent
142Type checking a file, if successful, creates a bytecode version of the file (in
143this case \texttt{hello.ibc}) to speed up loading in future. The bytecode is
144regenerated if the source file changes.