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