git.iko.soy/Idris-dev
on master help sign in
Idris-dev/docs/tutorial/packages.rst
185 lines 5.6 kB history raw
1.. _sect-packages:
3********
4Packages
5********
7Idris includes a simple build system for building packages and executables
8from a named package description file. These files can be used with the
9Idris compiler to manage the development process.
11Package Descriptions
12====================
14A package description includes the following:
16+ A header, consisting of the keyword ``package`` followed by a package
17 name. Package names can be any valid Idris identifier. The iPKG
18 format also takes a quoted version that accepts any valid filename.
20+ Fields describing package contents, ``<field> = <value>``.
22At least one field must be the modules field, where the value is a
23comma separated list of modules. For example, given an idris package
24``maths`` that has modules ``Maths.idr``, ``Maths.NumOps.idr``,
25``Maths.BinOps.idr``, and ``Maths.HexOps.idr``, the corresponding
26package file would be:
28::
30 package maths
32 modules = Maths
33 , Maths.NumOps
34 , Maths.BinOps
35 , Maths.HexOps
38Other examples of package files can be found in the ``libs`` directory
39of the main Idris repository, and in `third-party libraries
40<https://github.com/idris-lang/Idris-dev/wiki/Libraries>`_.
43Using Package files
44===================
46Idris itself is aware about packages, and special commands are
47available to help with, for example, building packages, installing
48packages, and cleaning packages. For instance, given the ``maths``
49package from earlier we can use Idris as follows:
51+ ``idris --build maths.ipkg`` will build all modules in the package
53+ ``idris --install maths.ipkg`` will install the package, making it
54 accessible by other Idris libraries and programs.
56+ ``idris --clean maths.ipkg`` will delete all intermediate code and
57 executable files generated when building.
59Once the maths package has been installed, the command line option
60``--package maths`` makes it accessible (abbreviated to ``-p maths``).
61For example:
63::
65 idris -p maths Main.idr
68Testing Idris Packages
69======================
71The integrated build system includes a simple testing framework.
72This framework collects functions listed in the ``ipkg`` file under ``tests``.
73All test functions must return ``IO ()``.
75When you enter ``idris --testpkg yourmodule.ipkg``,
76the build system creates a temporary file in a fresh environment on your machine
77by listing the ``tests`` functions under a single ``main`` function.
78It compiles this temporary file to an executable and then executes it.
80The tests themselves are responsible for reporting their success or failure.
81Test functions commonly use ``putStrLn`` to report test results.
82The test framework does not impose any standards for reporting and consequently
83does not aggregate test results.
85For example, lets take the following list of functions that are defined in a
86module called ``NumOps`` for a sample package ``maths``:
88.. name: Math/NumOps.idr
89.. code-block:: idris
91 module Maths.NumOps
93 %access export -- to make functions under test visible
95 double : Num a => a -> a
96 double a = a + a
98 triple : Num a => a -> a
99 triple a = a + double a
102A simple test module, with a qualified name of ``Test.NumOps`` can be declared as:
104.. name: Math/TestOps.idr
105.. code-block:: idris
107 module Test.NumOps
109 import Maths.NumOps
111 %access export -- to make the test functions visible
113 assertEq : Eq a => (given : a) -> (expected : a) -> IO ()
114 assertEq g e = if g == e
115 then putStrLn "Test Passed"
116 else putStrLn "Test Failed"
118 assertNotEq : Eq a => (given : a) -> (expected : a) -> IO ()
119 assertNotEq g e = if not (g == e)
120 then putStrLn "Test Passed"
121 else putStrLn "Test Failed"
123 testDouble : IO ()
124 testDouble = assertEq (double 2) 4
126 testTriple : IO ()
127 testTriple = assertNotEq (triple 2) 5
130The functions ``assertEq`` and ``assertNotEq`` are used to run expected passing,
131and failing, equality tests. The actual tests are ``testDouble`` and ``testTriple``,
132and are declared in the ``maths.ipkg`` file as follows:
134::
136 package maths
138 modules = Maths.NumOps
139 , Test.NumOps
141 tests = Test.NumOps.testDouble
142 , Test.NumOps.testTriple
145The testing framework can then be invoked using ``idris --testpkg maths.ipkg``:
147::
149 > idris --testpkg maths.ipkg
150 Type checking ./Maths/NumOps.idr
151 Type checking ./Test/NumOps.idr
152 Type checking /var/folders/63/np5g0d5j54x1s0z12rf41wxm0000gp/T/idristests144128232716531729.idr
153 Test Passed
154 Test Passed
156Note how both tests have reported success by printing ``Test Passed``
157as we arranged for with the ``assertEq`` and ``assertNoEq`` functions.
159Package Dependencies Using Atom
160===============================
162If you are using the Atom editor and have a dependency on another package,
163corresponding to for instance ``import Lightyear`` or ``import Pruviloj``,
164you need to let Atom know that it should be loaded. The easiest way to
165accomplish that is with a .ipkg file. The general contents of an ipkg file
166will be described in the next section of the tutorial, but for now here is
167a simple recipe for this trivial case:
169- Create a folder myProject.
171- Add a file myProject.ipkg containing just a couple of lines:
173.. code-block:: idris
175 package myProject
177 pkgs = pruviloj, lightyear
179- In Atom, use the File menu to Open Folder myProject.
181More information
182================
184More details, including a complete listing of available fields, can be
185found in the reference manual in :ref:`ref-sect-packages`.