@@ -1,13 +1,10 @@
7−Idris includes a simple system for building packages from a
6+Idris includes a simple build system for building packages and executables from a named package description file.
8−package description file. These files can be used with the Idris
9−compiler to manage the development process of your Idris
7+These files can be used with the Idris compiler to manage the development process .
10−programmes and packages.
12Package Descriptions
9Package Descriptions
13====================
10====================
@@ -18,84 +15,51 @@ A package description includes the following:
18+ Fields describing package contents, ``<field> = <value>``
15+ Fields describing package contents, ``<field> = <value>``
20At least one field must be the modules field, where the value is a
17At 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
18+comma separated list of modules. For example, given an idris package
22−has two modules ``foo.idr`` and ``bar.idr`` as source files would be
19+``maths`` that has modules ``Maths.idr``, ``Maths.NumOps.idr``,
23−written as follows::
20+``Maths.BinOps.idr``, and ``Maths.HexOps.idr``, the corresponding
21+package file would be::
25− package foo
25+ modules = Maths
29Other examples of package files can be found in the ``libs`` directory
31Other examples of package files can be found in the ``libs`` directory
30of the main Idris repository, and in `third-party libraries <https://github.com/idris-lang/Idris-dev/wiki/Libraries>`_.
32of 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`.
35−Other common fields which may be present in an ``ipkg`` file are:
37−+ ``sourcedir = <dir>``, which takes the directory (relative to the
38− current directory) which contains the source. Default is the current
41−+ ``executable = <output>``, which takes the name of the executable
44−+ ``main = <module>``, which takes the name of the main module, and
45− must be present if the executable field is present.
47−+ ``opts = "<idris options>"``, which allows options (such as other
48− packages) to be passed to Idris.
53−In more advanced cases, particularly to support creating bindings to
54−external ``C`` libraries, the following options are available:
56−+ ``makefile = <file>``, which specifies a ``Makefile``, to be built
57− before the Idris modules, for example to support linking with a
60−+ ``libs = <libs>``, which takes a comma separated list of libraries
61− which must be present for the package to be usable.
63−+ ``objs = <objs>``, which takes a comma separated list of additional
64− object files to be installed, perhaps generated by the ``Makefile``.
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:
73−+ ``tests = <test functions>``, which takes the qualified names of all test functions to be run.
76− The modules containing the test functions must also be added to the list of modules.
78Using Package files
36Using Package files
79===================
37===================
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:
83−+ ``idris --build test.ipkg`` will build all modules in the package
41++ ``idris --build maths.ipkg`` will build all modules in the package
85−+ ``idris --install test.ipkg`` will install the package, making it
43++ ``idris --install maths.ipkg`` will install the package, making it
86 accessible by other Idris libraries and programs.
44 accessible by other Idris libraries and programs.
88−+ ``idris --clean test.ipkg`` will delete all intermediate code and
46++ ``idris --clean maths.ipkg`` will delete all intermediate code and
89 executable files generated when building.
47 executable files generated when building.
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
53++ ``idris --checkpkg maths.ipkg`` will type check all modules in the
93−+ ``idris --checkpkg test.ipkg`` will type check all modules in the package only. This differs from build that type checks **and** generates code.
54+ package only. This differs from build that type checks **and**
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.
97−Once the test package has been installed, the command line option
61+Once the maths package has been installed, the command line option
98−``--package test`` makes it accessible (abbreviated to ``-p test``).
62+``--package maths`` makes it accessible (abbreviated to ``-p maths``).
99For example::
63For example::
101− idris -p test Main.idr
65+ idris -p maths Main.idr