@@ -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,60 +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::
2422
25− package foo
23+ package maths
24+
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−Other common fields which may be present in an ``ipkg`` file are:
33−
34−+ ``sourcedir = <dir>``, which gives the directory (relative to the
35− current directory) which contains the source. Default is the current
36− directory.
37−
38−+ ``executable = <output>``, which gives the name of the executable
39− file to generate.
40−
41−+ ``main = <module>``, which gives the name of the main module, and
42− must be present if the executable field is present.
43−
44−+ ``opts = "<idris options>"``, which allows options (such as other
45− packages) to be passed to Idris.
46−
47−In more advanced cases, particularly to support creating bindings to
48−external ``C`` libraries, the following options are available:
49−
50−+ ``makefile = <file>``, which specifies a ``Makefile``, to be built
51− before the Idris modules, for example to support linking with a
52− ``C`` library.
53−
54−+ ``libs = <libs>``, which gives a comma separated list of libraries
55− which must be present for the package to be usable.
56−
57−+ ``objs = <objs>``, which gives a comma separated list of additional
58− object files to be installed, perhaps generated by the ``Makefile``.
5935
6036Using Package files
6137===================
6238
63−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:
6440
65−+ ``idris --build test.ipkg`` will build all modules in the package
41++ ``idris --build maths.ipkg`` will build all modules in the package
6642
67−+ ``idris --install test.ipkg`` will install the package, making it
43++ ``idris --install maths.ipkg`` will install the package, making it
6844 accessible by other Idris libraries and programs.
6945
70−+ ``idris --clean test.ipkg`` will delete all intermediate code and
46++ ``idris --clean maths.ipkg`` will delete all intermediate code and
7147 executable files generated when building.
7248
73−Once the test package has been installed, the command line option
74−``--package test`` makes it accessible (abbreviated to ``-p test``).
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.
52+
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.
56+
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.
60+
61+Once the maths package has been installed, the command line option
62+``--package maths`` makes it accessible (abbreviated to ``-p maths``).
7563For example::
7664
77− idris -p test Main.idr
65+ idris -p maths Main.idr