git.iko.soy/Idris-dev
on dff4fcd help sign in
Idris-dev/docs/tutorial/starting.rst
92 lines 3.3 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 sufficiently recent, though it is better to be completely up to date.
15- The *GNU Multiple Precision Arithmetic Library* (GMP) is available from MacPorts/Homebrew and all major Linux distributions.
17Downloading and Installing
18==========================
20The easiest way to install Idris, if you have all of the
21prerequisites, is to type:
23::
25 cabal update; cabal install idris
27This will install the latest version released on Hackage, along with
28any dependencies. If, however, you would like the most up to date
29development version you can find it, as well as build instructions, on
30GitHub at: https://github.com/idris-lang/Idris-dev.
32If you haven't previously installed anything using Cabal, then Idris
33may not be on your path. Should the Idris executable not be found
34please ensure that you have added ``~/.cabal/bin`` to your ``$PATH``
35environment variable. Mac OS X users may find they need to add
36``~/Library/Haskell/bin`` instead, and Windows users will typically
37find that Cabal installs programs in ``%HOME%\AppData\Roaming\cabal\bin``.
39To check that installation has succeeded, and to write your first
40Idris program, create a file called ``hello.idr`` containing the
41following text:
43.. code-block:: idris
45 module Main
47 main : IO ()
48 main = putStrLn "Hello world"
50If you are familiar with Haskell, it should be fairly clear what the
51program is doing and how it works, but if not, we will explain the
52details later. You can compile the program to an executable by
53entering ``idris hello.idr -o hello`` at the shell prompt. This will
54create an executable called ``hello``, which you can run:
56::
58 $ idris hello.idr -o hello
59 $ ./hello
60 Hello world
62Please note that the dollar sign ``$`` indicates the shell prompt!
63Some useful options to the Idris command are:
65- ``-o prog`` to compile to an executable called ``prog``.
67- ``--check`` type check the file and its dependencies without starting the interactive environment.
69- ``--package pkg`` add package as dependency, e.g. ``--package contrib`` to make use of the contrib package.
71- ``--help`` display usage summary and command line options.
73The Interactive Environment
74===========================
76Entering ``idris`` at the shell prompt starts up the interactive
77environment. You should see something like the following:
79.. literalinclude:: ../listing/idris-prompt-start.txt
81This gives a ``ghci`` style interface which allows evaluation of, as
82well as type checking of, expressions; theorem proving, compilation;
83editing; and various other operations. The command ``:?`` gives a list
84of supported commands. Below, we see an example run in
85which ``hello.idr`` is loaded, the type of ``main`` is checked and
86then the program is compiled to the executable ``hello``. Type
87checking a file, if successful, creates a bytecode version of the file
88(in this case ``hello.ibc``) to speed up loading in future. The
89bytecode is regenerated if the source file changes.
91.. _run1:
92.. literalinclude:: ../listing/idris-prompt-helloworld.txt