git.iko.soy/Idris-dev
on master help sign in
Updates to User Docs on Idris packages.
efd9950Jan de Muijnck-Hughes
docs/reference/packages.rst+4−2
compare with master
unifiedsplit
@@ -97,7 +97,7 @@ external ``C`` libraries, the following options are available:
97 which must be present for the package to be usable.
97 which must be present for the package to be usable.
98
98
99+ ``objs = <objs>``, which takes a comma separated list of additional
99+ ``objs = <objs>``, which takes a comma separated list of additional
100− files to be installed (object files, headers), perhaps generated
100+ files to be installed (object files, headers), perhaps generated
101 by the ``Makefile``.
101 by the ``Makefile``.
102
102
103Testing
103Testing
@@ -111,7 +111,7 @@ The following option is available:
111
111
112.. IMPORTANT::
112.. IMPORTANT::
113 The modules containing the test functions must also be added to the list of modules.
113 The modules containing the test functions must also be added to the list of modules.
114−
114+
115Comments
115Comments
116---------
116---------
117
117
@@ -132,6 +132,8 @@ Given an Idris package file ``text.ipkg`` it can be used with the Idris compiler
132
132
133+ ``idris --mkdoc test.ipkg`` will build HTML documentation for your package in the folder ``test_doc`` in your project's root directory.
133+ ``idris --mkdoc test.ipkg`` will build HTML documentation for your package in the folder ``test_doc`` in your project's root directory.
134
134
135++ ``idris --installdoc test.ipkg`` will install the packages documentation into Idris' central documentation folder located at ``idris --docdir``.
136+
135+ ``idris --checkpkg test.ipkg`` will type check all modules in the package only. This differs from build that type checks **and** generates code.
137+ ``idris --checkpkg test.ipkg`` will type check all modules in the package only. This differs from build that type checks **and** generates code.
136
138
137+ ``idris --testpkg test.ipkg`` will compile and run any embedded tests you have specified in the ``tests`` parameter.
139+ ``idris --testpkg test.ipkg`` will compile and run any embedded tests you have specified in the ``tests`` parameter.
docs/tutorial/index.rst−1
@@ -24,7 +24,6 @@ This is the Idris Tutorial. It will teach you about programming in the Idris Lan
24 interfaces
24 interfaces
25 modules
25 modules
26 packages
26 packages
27− testing
28 interp
27 interp
29 views
28 views
30 theorems
29 theorems
docs/tutorial/packages.rst+101−15
@@ -31,14 +31,18 @@ package file would be::
31
31
32
32
33Other examples of package files can be found in the ``libs`` directory
33Other examples of package files can be found in the ``libs`` directory
34−of the main Idris repository, and in `third-party libraries <https://github.com/idris-lang/Idris-dev/wiki/Libraries>`_.
34+of the main Idris repository, and in `third-party libraries
35−More details including a complete listing of available fields can be found in :ref:`ref-sect-packages`.
35+<https://github.com/idris-lang/Idris-dev/wiki/Libraries>`_.
36
36
37
37
38Using Package files
38Using Package files
39===================
39===================
40
40
41−Given an Idris package file ``maths.ipkg`` it can be used with the Idris compiler as follows:
41+
42+Idris itself is aware about packages, and special commands are
43+available to help with, for example, building packages, installing
44+packages, and cleaning packages. For instance, given the ``maths``
45+package from earlier we can use Idris as follows:
42
46
43+ ``idris --build maths.ipkg`` will build all modules in the package
47+ ``idris --build maths.ipkg`` will build all modules in the package
44
48
@@ -48,20 +52,102 @@ Given an Idris package file ``maths.ipkg`` it can be used with the Idris compile
48+ ``idris --clean maths.ipkg`` will delete all intermediate code and
52+ ``idris --clean maths.ipkg`` will delete all intermediate code and
49 executable files generated when building.
53 executable files generated when building.
50
54
51−+ ``idris --mkdoc maths.ipkg`` will build HTML documentation for your
52− package in the folder ``maths_doc`` in your project's root
53− directory.
54−
55−+ ``idris --checkpkg maths.ipkg`` will type check all modules in the
56− package only. This differs from build that type checks **and**
57− generates code.
58−
59−+ ``idris --testpkg maths.ipkg`` will compile and run any embedded
60− tests you have specified in the ``tests`` parameter. More
61− information about testing is given in the next section.
62−
63Once the maths package has been installed, the command line option
55Once the maths package has been installed, the command line option
64``--package maths`` makes it accessible (abbreviated to ``-p maths``).
56``--package maths`` makes it accessible (abbreviated to ``-p maths``).
65For example::
57For example::
66
58
67 idris -p maths Main.idr
59 idris -p maths Main.idr
60+
61+
62+Testing Idris Packages
63+======================
64+
65+The integrated build system includes a simple testing framework.
66+This framework collects functions listed in the ``ipkg`` file under ``tests``.
67+All test functions must return ``IO ()``.
68+
69+
70+When you enter ``idris --testpkg yourmodule.ipkg``,
71+the build system creates a temporary file in a fresh environment on your machine
72+by listing the ``tests`` functions under a single ``main`` function.
73+It compiles this temporary file to an executable and then executes it.
74+
75+
76+The tests themselves are responsible for reporting their success or failure.
77+Test functions commonly use ``putStrLn`` to report test results.
78+The test framework does not impose any standards for reporting and consequently
79+does not aggregate test results.
80+
81+
82+For example, lets take the following list of functions that are defined in a module called ``NumOps`` for a sample package ``maths``.
83+
84+.. name: Math/NumOps.idr
85+.. code-block:: idris
86+
87+ module Maths.NumOps
88+
89+ %access export -- to make functions under test visible
90+
91+ double : Num a => a -> a
92+ double a = a + a
93+
94+ triple : Num a => a -> a
95+ triple a = a + double a
96+
97+A simple test module, with a qualified name of ``Test.NumOps`` can be declared as
98+
99+.. name: Math/TestOps.idr
100+.. code-block:: idris
101+
102+ module Test.NumOps
103+
104+ import Maths.NumOps
105+
106+ %access export -- to make the test functions visible
107+
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"
112+
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"
117+
118+ testDouble : IO ()
119+ testDouble = assertEq (double 2) 4
120+
121+ testTriple : IO ()
122+ testTriple = assertNotEq (triple 2) 5
123+
124+
125+The functions ``assertEq`` and ``assertNotEq`` are used to run expected passing, and failing, equality tests.
126+The actual tests are ``testDouble`` and ``testTriple``, and are declared in the ``maths.ipkg`` file as follows::
127+
128+ package maths
129+
130+ modules = Maths.NumOps
131+ , Test.NumOps
132+
133+ tests = Test.NumOps.testDouble
134+ , Test.NumOps.testTriple
135+
136+
137+The testing framework can then be invoked using ``idris --testpkg maths.ipkg``::
138+
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
145+
146+Note how both tests have reported success by printing ``Test Passed``
147+as we arranged for with the ``assertEq`` and ``assertNoEq`` functions.
148+
149+More information
150+================
151+
152+More details, including a complete listing of available fields, can be
153+found in the reference manual in :ref:`ref-sect-packages`.
docs/tutorial/testing.rstdeleted−89
@@ -1,89 +0,0 @@
1−.. _tut-sect-testing:
2−
3−**********************
4−Testing Idris Packages
5−**********************
6−
7−The integrated build system includes a simple testing framework.
8−This framework collects functions listed in the ``ipkg`` file under ``tests``.
9−All test functions must return ``IO ()``.
10−
11−
12−When you enter ``idris --testpkg yourmodule.ipkg``,
13−the build system creates a temporary file in a fresh environment on your machine
14−by listing the ``tests`` functions under a single ``main`` function.
15−It compiles this temporary file to an executable and then executes it.
16−
17−
18−The tests themselves are responsible for reporting their success or failure.
19−Test functions commonly use ``putStrLn`` to report test results.
20−The test framework does not impose any standards for reporting and consequently
21−does not aggregate test results.
22−
23−
24−For example, lets take the following list of functions that are defined in a module called ``NumOps`` for a sample package ``maths``.
25−
26−.. name: Math/NumOps.idr
27−.. code-block:: idris
28−
29− module Maths.NumOps
30−
31− %access export -- to make functions under test visible
32−
33− double : Num a => a -> a
34− double a = a + a
35−
36− triple : Num a => a -> a
37− triple a = a + double a
38−
39−A simple test module, with a qualified name of ``Test.NumOps`` can be declared as
40−
41−.. name: Math/TestOps.idr
42−.. code-block:: idris
43−
44− module Test.NumOps
45−
46− import Maths.NumOps
47−
48− %access export -- to make the test functions visible
49−
50− assertEq : Eq a => (given : a) -> (expected : a) -> IO ()
51− assertEq g e = if g == e
52− then putStrLn "Test Passed"
53− else putStrLn "Test Failed"
54−
55− assertNotEq : Eq a => (given : a) -> (expected : a) -> IO ()
56− assertNotEq g e = if not (g == e)
57− then putStrLn "Test Passed"
58− else putStrLn "Test Failed"
59−
60− testDouble : IO ()
61− testDouble = assertEq (double 2) 4
62−
63− testTriple : IO ()
64− testTriple = assertNotEq (triple 2) 5
65−
66−
67−The functions ``assertEq`` and ``assertNotEq`` are used to run expected passing, and failing, equality tests.
68−The actual tests are ``testDouble`` and ``testTriple``, and are declared in the ``maths.ipkg`` file as follows::
69−
70− package maths
71−
72− modules = Maths.NumOps
73− , Test.NumOps
74−
75− tests = Test.NumOps.testDouble
76− , Test.NumOps.testTriple
77−
78−
79−The testing framework can then be invoked using ``idris --testpkg maths.ipkg``::
80−
81− > idris --testpkg maths.ipkg
82− Type checking ./Maths/NumOps.idr
83− Type checking ./Test/NumOps.idr
84− Type checking /var/folders/63/np5g0d5j54x1s0z12rf41wxm0000gp/T/idristests144128232716531729.idr
85− Test Passed
86− Test Passed
87−
88−Note how both tests have reported success by printing ``Test Passed``
89−as we arranged for with the ``assertEq`` and ``assertNoEq`` functions.