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