git.iko.soy/Idris-dev
on 465cc1c help sign in
Idris-dev/docs/tutorial/starting.rst
84 lines 2.9 kB history raw
1.. _sect-starting:
3===============
4Getting Started
5===============
7Prerequisites
8-------------
10Before installing Idris, you will need to make sure you have all
11of the 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
15 date.
17- The *GNU Multiple Precision Arithmetic Library* (GMP) is available
18 from MacPorts/Homebrew and all major Linux distributions.
20Downloading and Installing
21--------------------------
23The easiest way to install Idris, if you have all of the
24prerequisites, is to type:
26::
28 cabal update; cabal install idris
30This will install the latest version released on Hackage, along with
31any dependencies. If, however, you would like the most up to date
32development version you can find it, as well as build intructions, on
33GitHub at: https://github.com/idris-lang/Idris-dev.
35To check that installation has succeeded, and to write your first
36Idris program, create a file called “``hello.idr``” containing the
37following text:
39If you are familiar with Haskell, it should be fairly clear what the
40program is doing and how it works, but if not, we will explain the
41details later. You can compile the program to an executable by
42entering ``idris hello.idr -o hello`` at the shell prompt. This will
43create an executable called ``hello``, which you can run:
45::
47 $ idris hello.idr -o hello
48 $ ./hello
49 Hello world
51Note that the ``$`` indicates the shell prompt! Should the Idris
52executable not be found please ensure that you have added
53``~/.cabal/bin`` to your ``$PATH`` environment variable. Mac OS X
54users may find they need to use ``~/Library/Haskell/bin``
55instead. Some useful options to the Idris command are:
57- ``-o prog`` to compile to an executable called ``prog``.
59- ``--check`` type check the file and its dependencies without
60 starting the interactive environment.
62- ``--help`` display usage summary and command line options
64The Interactive Environment
65---------------------------
67Entering ``idris`` at the shell prompt starts up the interactive
68environment. You should see something like the following:
70.. literalinclude:: ../listing/idris-prompt-start.txt
72This gives a ``ghci`` style interface which allows evaluation of, as
73well as type checking of, expressions; theorem proving, compilation;
74editing; and various other operations. The command ``:?`` gives a list
75of supported commands. Listing :ref:`run1` shows an example run in
76which ``hello.idr`` is loaded, the type of ``main`` is checked and
77then the program is compiled to the executable ``hello``. Type
78checking a file, if successful, creates a bytecode version of the file
79(in this case ``hello.ibc``) to speed up loading in future. The
80bytecode is regenerated if the source file changes.
82.. literalinclude:: ../listing/idris-prompt-helloworld.txt
83 :caption: Sample Interactive Run
84 :name: run1