@@ -1,13 +1,10 @@
1−.. _sect-packages:
2−
31********
42Packages
53********
64
7−Idris includes a simple system for building packages from a
8−package description file. These files can be used with the Idris
9−compiler to manage the development process of your Idris
10−programmes and packages.
5+
6+Idris includes a simple build system for building packages and executables from a named package description file.
7+These files can be used with the Idris compiler to manage the development process .
118
129Package Descriptions
1310====================
@@ -18,84 +15,51 @@ A package description includes the following:
1815+ Fields describing package contents, ``<field> = <value>``
1916
2017At least one field must be the modules field, where the value is a
21−comma separated list of modules. For example, a library test which
22−has two modules ``foo.idr`` and ``bar.idr`` as source files would be
23−written as follows::
18+comma separated list of modules. For example, given an idris package
19+``maths`` that has modules ``Maths.idr``, ``Maths.NumOps.idr``,
20+``Maths.BinOps.idr``, and ``Maths.HexOps.idr``, the corresponding
21+package file would be::
22+
23+ package maths
2424
25− package foo
25+ modules = Maths
26+ , Maths.NumOps
27+ , Maths.BinOps
28+ , Maths.HexOps
2629
27− modules = foo, bar
2830
2931Other examples of package files can be found in the ``libs`` directory
3032of the main Idris repository, and in `third-party libraries <https://github.com/idris-lang/Idris-dev/wiki/Libraries>`_.
33+More details including a complete listing of available fields can be found in :ref:`ref-sect-packages`.
3134
32−Common Fields
33−-------------
34−
35−Other common fields which may be present in an ``ipkg`` file are:
36−
37−+ ``sourcedir = <dir>``, which takes the directory (relative to the
38− current directory) which contains the source. Default is the current
39− directory.
40−
41−+ ``executable = <output>``, which takes the name of the executable
42− file to generate.
43−
44−+ ``main = <module>``, which takes the name of the main module, and
45− must be present if the executable field is present.
46−
47−+ ``opts = "<idris options>"``, which allows options (such as other
48− packages) to be passed to Idris.
49−
50−Binding to C
51−------------
52−
53−In more advanced cases, particularly to support creating bindings to
54−external ``C`` libraries, the following options are available:
55−
56−+ ``makefile = <file>``, which specifies a ``Makefile``, to be built
57− before the Idris modules, for example to support linking with a
58− ``C`` library.
59−
60−+ ``libs = <libs>``, which takes a comma separated list of libraries
61− which must be present for the package to be usable.
62−
63−+ ``objs = <objs>``, which takes a comma separated list of additional
64− object files to be installed, perhaps generated by the ``Makefile``.
65−
66−Testing
67−--------
68−
69−For testing Idris packages, there is a rudimentary testing harness, which is run in the ``IO`` context, built into Idris.
70−This allows for testing modules containting functions that test aspects of your package to be run automatically in a fresh environment on your computer.
71−All test functions must return ``IO ()``, and are listed in the ``ipkg`` file using the field:
72−
73−+ ``tests = <test functions>``, which takes the qualified names of all test functions to be run.
74−
75−.. IMPORTANT::
76− The modules containing the test functions must also be added to the list of modules.
7735
7836Using Package files
7937===================
8038
81−Given an Idris package file ``text.ipkg`` it can be used with the Idris compiler as follows:
39+Given an Idris package file ``maths.ipkg`` it can be used with the Idris compiler as follows:
8240
83−+ ``idris --build test.ipkg`` will build all modules in the package
41++ ``idris --build maths.ipkg`` will build all modules in the package
8442
85−+ ``idris --install test.ipkg`` will install the package, making it
43++ ``idris --install maths.ipkg`` will install the package, making it
8644 accessible by other Idris libraries and programs.
8745
88−+ ``idris --clean test.ipkg`` will delete all intermediate code and
46++ ``idris --clean maths.ipkg`` will delete all intermediate code and
8947 executable files generated when building.
9048
91−+ ``idris --mkdoc test.ipkg`` will build HTML documentation for your package in the folder ``test_doc`` in your project's root directory.
49++ ``idris --mkdoc maths.ipkg`` will build HTML documentation for your
50+ package in the folder ``maths_doc`` in your project's root
51+ directory.
9252
93−+ ``idris --checkpkg test.ipkg`` will type check all modules in the package only. This differs from build that type checks **and** generates code.
53++ ``idris --checkpkg maths.ipkg`` will type check all modules in the
54+ package only. This differs from build that type checks **and**
55+ generates code.
9456
95−+ ``idris --testpkg test.ipkg`` will compile and run any embedded tests you have specified in the ``tests`` paramater.
57++ ``idris --mathspkg maths.ipkg`` will compile and run any embedded
58+ mathss you have specified in the ``tests`` paramater. More
59+ information about mathsing is given in the next section.
9660
97−Once the test package has been installed, the command line option
98−``--package test`` makes it accessible (abbreviated to ``-p test``).
61+Once the maths package has been installed, the command line option
62+``--package maths`` makes it accessible (abbreviated to ``-p maths``).
9963For example::
10064
101− idris -p test Main.idr
65+ idris -p maths Main.idr