Idris includes a simple build system for building packages and executables from a named package description file. These files can be used with the Idris compiler to manage the development process .
A package description includes the following:
- A header, consisting of the keyword package followed by the package name. Package names can be any valid Idris identifier. The iPKG format also takes a quoted version that accepts any valid filename.
- Fields describing package contents,
<field> = <value>
At least one field must be the modules field, where the value is a
comma separated list of modules. For example, given an idris package
maths that has modules
Maths.HexOps.idr, the corresponding
package file would be:
package maths modules = Maths , Maths.NumOps , Maths.BinOps , Maths.HexOps
Other examples of package files can be found in the
of the main Idris repository, and in third-party libraries.
Using Package files¶
Idris itself is aware about packages, and special commands are
available to help with, for example, building packages, installing
packages, and cleaning packages. For instance, given the
package from earlier we can use Idris as follows:
idris --build maths.ipkgwill build all modules in the package
idris --install maths.ipkgwill install the package, making it accessible by other Idris libraries and programs.
idris --clean maths.ipkgwill delete all intermediate code and executable files generated when building.
Once the maths package has been installed, the command line option
--package maths makes it accessible (abbreviated to
idris -p maths Main.idr
Testing Idris Packages¶
The integrated build system includes a simple testing framework.
This framework collects functions listed in the
ipkg file under
All test functions must return
When you enter
idris --testpkg yourmodule.ipkg,
the build system creates a temporary file in a fresh environment on your machine
by listing the
tests functions under a single
It compiles this temporary file to an executable and then executes it.
The tests themselves are responsible for reporting their success or failure.
Test functions commonly use
putStrLn to report test results.
The test framework does not impose any standards for reporting and consequently
does not aggregate test results.
For example, lets take the following list of functions that are defined in a module called
NumOps for a sample package
module Maths.NumOps %access export -- to make functions under test visible double : Num a => a -> a double a = a + a triple : Num a => a -> a triple a = a + double a
A simple test module, with a qualified name of
Test.NumOps can be declared as
module Test.NumOps import Maths.NumOps %access export -- to make the test functions visible assertEq : Eq a => (given : a) -> (expected : a) -> IO () assertEq g e = if g == e then putStrLn "Test Passed" else putStrLn "Test Failed" assertNotEq : Eq a => (given : a) -> (expected : a) -> IO () assertNotEq g e = if not (g == e) then putStrLn "Test Passed" else putStrLn "Test Failed" testDouble : IO () testDouble = assertEq (double 2) 4 testTriple : IO () testTriple = assertNotEq (triple 2) 5
assertNotEq are used to run expected passing, and failing, equality tests.
The actual tests are
testTriple, and are declared in the
maths.ipkg file as follows:
package maths modules = Maths.NumOps , Test.NumOps tests = Test.NumOps.testDouble , Test.NumOps.testTriple
The testing framework can then be invoked using
idris --testpkg maths.ipkg:
> idris --testpkg maths.ipkg Type checking ./Maths/NumOps.idr Type checking ./Test/NumOps.idr Type checking /var/folders/63/np5g0d5j54x1s0z12rf41wxm0000gp/T/idristests144128232716531729.idr Test Passed Test Passed
Note how both tests have reported success by printing
as we arranged for with the