git.iko.soy/Idris-dev
on f572cd0 help sign in
Idris-dev/docs/tutorial/starting.rst
109 lines 3.5 kB history raw
1.. _sect-starting:
3===============
4Getting Started
5===============
7Prerequisites
8-------------
10Before installing ``Idris``, you will need to make sure you have all of
11the necessary libraries and tools. You will need:
13- A fairly recent Haskell platform. Version 2013.2.0.0 should be
14 sufficiently recent, though it is better to be completely up to date.
16- The *GNU Multiple Precision Arithmetic Library* (GMP) is available
17 from MacPorts/Homebrew and all major Linux distributions.
19Downloading and Installing
20--------------------------
22The easiest way to install ``Idris``, if you have all of the
23prerequisites, is to type:
25::
27 cabal update; cabal install idris
29This will install the latest version released on Hackage, along with any
30dependencies. If, however, you would like the most up to date
31development version you can find it, as well as build intructions, on
32GitHub at: https://github.com/edwinb/Idris-dev.
34To check that installation has succeeded, and to write your first
35``Idris`` program, create a file called “``hello.idr``” containing the
36following text:
38If you are familiar with Haskell, it should be fairly clear what the
39program is doing and how it works, but if not, we will explain the
40details later. You can compile the program to an executable by entering
41``idris hello.idr -o hello`` at the shell prompt. This will create an
42executable called ``hello``, which you can run:
44::
46 $ idris hello.idr -o hello
47 $ ./hello
48 Hello world
50Note that the ``$`` indicates the shell prompt! Should the ``Idris``
51executable not be found please ensure that you have added
52``~/.cabal/bin`` to your ``$PATH`` environment variable. Mac OS X users
53may find they need to use ``~/Library/Haskell/bin`` instead. Some useful
54options to the ``Idris`` command are:
56- ``-o prog`` to compile to an executable called ``prog``.
58- ``--check`` type check the file and its dependencies without starting
59 the interactive environment.
61- ``--help`` display usage summary and command line options
63The Interactive Environment
64---------------------------
66Entering ``idris`` at the shell prompt starts up the interactive
67environment. You should see something like the following:
69::
71 $ idris
72 ____ __ _
73 / _/___/ /____(_)____
74 / // __ / ___/ / ___/ Version 0.9.17
75 _/ // /_/ / / / (__ ) http://www.idris-lang.org/
76 /___/\__,_/_/ /_/____/ Type :? for help
78 Idris>
80This gives a ``ghci`` style interface which allows evaluation of, as
81well as type checking of, expressions; theorem proving, compilation;
82editing; and various other operations. The command ``:?`` gives a list
83of supported commands. Listing :ref:`run1` shows an example run in which
84``hello.idr`` is loaded, the type of ``main`` is checked and then the
85program is compiled to the executable ``hello``. Type checking a file,
86if successful, creates a bytecode version of the file (in this case
87``hello.ibc``) to speed up loading in future. The bytecode is
88regenerated if the source file changes.
90.. _run1:
92.. code-block:: bash
93 :caption: Sample Interactive Run
95 $ idris hello.idr
96 ____ __ _
97 / _/___/ /____(_)____
98 / // __ / ___/ / ___/ Version 0.9.17
99 _/ // /_/ / / / (__ ) http://www.idris-lang.org/
100 /___/\__,_/_/ /_/____/ Type :? for help
102 Type checking ./hello.idr
103 *hello> :t main
104 Main.main : IO ()
105 *hello> :c hello
106 *hello> :q
107 Bye bye
108 $ ./hello
109 Hello world