mirror of
https://github.com/ilyakooo0/Idris-dev.git
synced 2024-11-11 14:57:30 +03:00
Updates
+ Moved package listings to reference manual. + Added compact package description to tutorial. + Added section on testing idris packages.
This commit is contained in:
Jan de Muijnck-Hughes
parent
8b46d8f138
commit
9f042575e1
@ -39,6 +39,7 @@ The Idris Tutorial
|
||||
tutorial/classes
|
||||
tutorial/modules
|
||||
tutorial/packages
|
||||
tutorial/testing
|
||||
tutorial/interp
|
||||
tutorial/views
|
||||
tutorial/theorems
|
||||
@ -101,6 +102,7 @@ Language Reference
|
||||
:maxdepth: 1
|
||||
|
||||
reference/documenting
|
||||
reference/packages
|
||||
reference/uniqueness-types
|
||||
reference/ffi
|
||||
reference/erasure
|
||||
|
||||
@ -21,6 +21,7 @@ This will tell you how Idris works, for using it you should read the Idris Tutor
|
||||
:maxdepth: 1
|
||||
|
||||
documenting
|
||||
packages
|
||||
uniqueness-types
|
||||
ffi
|
||||
erasure
|
||||
@ -33,5 +34,3 @@ This will tell you how Idris works, for using it you should read the Idris Tutor
|
||||
language-extensions
|
||||
elaborator-reflection
|
||||
misc
|
||||
|
||||
|
||||
|
||||
101
docs/reference/packages.rst
Normal file
101
docs/reference/packages.rst
Normal file
@ -0,0 +1,101 @@
|
||||
.. _ref-sect-packages:
|
||||
|
||||
********
|
||||
Packages
|
||||
********
|
||||
|
||||
Idris includes a simple system for building packages from a
|
||||
package description file. These files can be used with the Idris
|
||||
compiler to manage the development process of your Idris
|
||||
programmes and packages.
|
||||
|
||||
Package Descriptions
|
||||
====================
|
||||
|
||||
A package description includes the following:
|
||||
|
||||
+ A header, consisting of the keyword package followed by the package name.
|
||||
+ 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, a library test which
|
||||
has two modules ``foo.idr`` and ``bar.idr`` as source files would be
|
||||
written as follows::
|
||||
|
||||
package foo
|
||||
|
||||
modules = foo, bar
|
||||
|
||||
Other examples of package files can be found in the ``libs`` directory
|
||||
of the main Idris repository, and in `third-party libraries <https://github.com/idris-lang/Idris-dev/wiki/Libraries>`_.
|
||||
|
||||
Common Fields
|
||||
-------------
|
||||
|
||||
Other common fields which may be present in an ``ipkg`` file are:
|
||||
|
||||
+ ``sourcedir = <dir>``, which takes the directory (relative to the
|
||||
current directory) which contains the source. Default is the current
|
||||
directory.
|
||||
|
||||
+ ``executable = <output>``, which takes the name of the executable
|
||||
file to generate.
|
||||
|
||||
+ ``main = <module>``, which takes the name of the main module, and
|
||||
must be present if the executable field is present.
|
||||
|
||||
+ ``opts = "<idris options>"``, which allows options (such as other
|
||||
packages) to be passed to Idris.
|
||||
|
||||
Binding to C
|
||||
------------
|
||||
|
||||
In more advanced cases, particularly to support creating bindings to
|
||||
external ``C`` libraries, the following options are available:
|
||||
|
||||
+ ``makefile = <file>``, which specifies a ``Makefile``, to be built
|
||||
before the Idris modules, for example to support linking with a
|
||||
``C`` library.
|
||||
|
||||
+ ``libs = <libs>``, which takes a comma separated list of libraries
|
||||
which must be present for the package to be usable.
|
||||
|
||||
+ ``objs = <objs>``, which takes a comma separated list of additional
|
||||
object files to be installed, perhaps generated by the ``Makefile``.
|
||||
|
||||
Testing
|
||||
--------
|
||||
|
||||
For testing Idris packages there is a rudimentary testing harness, run in the ``IO`` context.
|
||||
The ``iPKG`` file is used to specify the functions used for testing.
|
||||
The following option is available:
|
||||
|
||||
+ ``tests = <test functions>``, which takes the qualified names of all test functions to be run.
|
||||
|
||||
.. IMPORTANT::
|
||||
The modules containing the test functions must also be added to the list of modules.
|
||||
|
||||
Using Package files
|
||||
===================
|
||||
|
||||
Given an Idris package file ``text.ipkg`` it can be used with the Idris compiler as follows:
|
||||
|
||||
+ ``idris --build test.ipkg`` will build all modules in the package
|
||||
|
||||
+ ``idris --install test.ipkg`` will install the package, making it
|
||||
accessible by other Idris libraries and programs.
|
||||
|
||||
+ ``idris --clean test.ipkg`` will delete all intermediate code and
|
||||
executable files generated when building.
|
||||
|
||||
+ ``idris --mkdoc test.ipkg`` will build HTML documentation for your package in the folder ``test_doc`` in your project's root directory.
|
||||
|
||||
+ ``idris --checkpkg test.ipkg`` will type check all modules in the package only. This differs from build that type checks **and** generates code.
|
||||
|
||||
+ ``idris --testpkg test.ipkg`` will compile and run any embedded tests you have specified in the ``tests`` paramater.
|
||||
|
||||
Once the test package has been installed, the command line option
|
||||
``--package test`` makes it accessible (abbreviated to ``-p test``).
|
||||
For example::
|
||||
|
||||
idris -p test Main.idr
|
||||
@ -24,6 +24,7 @@ The is the Idris Tutorial. It will teach you about programming in the Idris Lang
|
||||
classes
|
||||
modules
|
||||
packages
|
||||
testing
|
||||
interp
|
||||
views
|
||||
theorems
|
||||
|
||||
@ -1,13 +1,10 @@
|
||||
.. _sect-packages:
|
||||
|
||||
********
|
||||
Packages
|
||||
********
|
||||
|
||||
Idris includes a simple system for building packages from a
|
||||
package description file. These files can be used with the Idris
|
||||
compiler to manage the development process of your Idris
|
||||
programmes and packages.
|
||||
|
||||
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 .
|
||||
|
||||
Package Descriptions
|
||||
====================
|
||||
@ -18,84 +15,51 @@ A package description includes the following:
|
||||
+ 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, a library test which
|
||||
has two modules ``foo.idr`` and ``bar.idr`` as source files would be
|
||||
written as follows::
|
||||
comma separated list of modules. For example, given an idris package
|
||||
``maths`` that has modules ``Maths.idr``, ``Maths.NumOps.idr``,
|
||||
``Maths.BinOps.idr``, and ``Maths.HexOps.idr``, the corresponding
|
||||
package file would be::
|
||||
|
||||
package foo
|
||||
package maths
|
||||
|
||||
modules = Maths
|
||||
, Maths.NumOps
|
||||
, Maths.BinOps
|
||||
, Maths.HexOps
|
||||
|
||||
modules = foo, bar
|
||||
|
||||
Other examples of package files can be found in the ``libs`` directory
|
||||
of the main Idris repository, and in `third-party libraries <https://github.com/idris-lang/Idris-dev/wiki/Libraries>`_.
|
||||
More details including a complete listing of available fields can be found in :ref:`ref-sect-packages`.
|
||||
|
||||
Common Fields
|
||||
-------------
|
||||
|
||||
Other common fields which may be present in an ``ipkg`` file are:
|
||||
|
||||
+ ``sourcedir = <dir>``, which takes the directory (relative to the
|
||||
current directory) which contains the source. Default is the current
|
||||
directory.
|
||||
|
||||
+ ``executable = <output>``, which takes the name of the executable
|
||||
file to generate.
|
||||
|
||||
+ ``main = <module>``, which takes the name of the main module, and
|
||||
must be present if the executable field is present.
|
||||
|
||||
+ ``opts = "<idris options>"``, which allows options (such as other
|
||||
packages) to be passed to Idris.
|
||||
|
||||
Binding to C
|
||||
------------
|
||||
|
||||
In more advanced cases, particularly to support creating bindings to
|
||||
external ``C`` libraries, the following options are available:
|
||||
|
||||
+ ``makefile = <file>``, which specifies a ``Makefile``, to be built
|
||||
before the Idris modules, for example to support linking with a
|
||||
``C`` library.
|
||||
|
||||
+ ``libs = <libs>``, which takes a comma separated list of libraries
|
||||
which must be present for the package to be usable.
|
||||
|
||||
+ ``objs = <objs>``, which takes a comma separated list of additional
|
||||
object files to be installed, perhaps generated by the ``Makefile``.
|
||||
|
||||
Testing
|
||||
--------
|
||||
|
||||
For testing Idris packages, there is a rudimentary testing harness, which is run in the ``IO`` context, built into Idris.
|
||||
This allows for testing modules containting functions that test aspects of your package to be run automatically in a fresh environment on your computer.
|
||||
All test functions must return ``IO ()``, and are listed in the ``ipkg`` file using the field:
|
||||
|
||||
+ ``tests = <test functions>``, which takes the qualified names of all test functions to be run.
|
||||
|
||||
.. IMPORTANT::
|
||||
The modules containing the test functions must also be added to the list of modules.
|
||||
|
||||
Using Package files
|
||||
===================
|
||||
|
||||
Given an Idris package file ``text.ipkg`` it can be used with the Idris compiler as follows:
|
||||
Given an Idris package file ``maths.ipkg`` it can be used with the Idris compiler as follows:
|
||||
|
||||
+ ``idris --build test.ipkg`` will build all modules in the package
|
||||
+ ``idris --build maths.ipkg`` will build all modules in the package
|
||||
|
||||
+ ``idris --install test.ipkg`` will install the package, making it
|
||||
+ ``idris --install maths.ipkg`` will install the package, making it
|
||||
accessible by other Idris libraries and programs.
|
||||
|
||||
+ ``idris --clean test.ipkg`` will delete all intermediate code and
|
||||
+ ``idris --clean maths.ipkg`` will delete all intermediate code and
|
||||
executable files generated when building.
|
||||
|
||||
+ ``idris --mkdoc test.ipkg`` will build HTML documentation for your package in the folder ``test_doc`` in your project's root directory.
|
||||
+ ``idris --mkdoc maths.ipkg`` will build HTML documentation for your
|
||||
package in the folder ``maths_doc`` in your project's root
|
||||
directory.
|
||||
|
||||
+ ``idris --checkpkg test.ipkg`` will type check all modules in the package only. This differs from build that type checks **and** generates code.
|
||||
+ ``idris --checkpkg maths.ipkg`` will type check all modules in the
|
||||
package only. This differs from build that type checks **and**
|
||||
generates code.
|
||||
|
||||
+ ``idris --testpkg test.ipkg`` will compile and run any embedded tests you have specified in the ``tests`` paramater.
|
||||
+ ``idris --mathspkg maths.ipkg`` will compile and run any embedded
|
||||
mathss you have specified in the ``tests`` paramater. More
|
||||
information about mathsing is given in the next section.
|
||||
|
||||
Once the test package has been installed, the command line option
|
||||
``--package test`` makes it accessible (abbreviated to ``-p test``).
|
||||
Once the maths package has been installed, the command line option
|
||||
``--package maths`` makes it accessible (abbreviated to ``-p maths``).
|
||||
For example::
|
||||
|
||||
idris -p test Main.idr
|
||||
idris -p maths Main.idr
|
||||
|
||||
66
docs/tutorial/testing.rst
Normal file
66
docs/tutorial/testing.rst
Normal file
@ -0,0 +1,66 @@
|
||||
.. _tut-sect-testing:
|
||||
|
||||
**********************
|
||||
Testing Idris Packages
|
||||
**********************
|
||||
|
||||
As part of the integrated build system a simple testing framework is provided.
|
||||
This framework will collect a list of named functions and construct an Idris executable in a fresh environment on your machine.
|
||||
This executable lists the named functions under a single ``main`` function, and imports the complete list of modules for the package.
|
||||
|
||||
|
||||
It is up to the developer to ensure the correct reporting of test results, and the structure and nature of how the tests are run.
|
||||
Further, all test functions must return ``IO ()``, and must be listed in the ``ipkg`` file under ``tests``, and rhe modules containing the test functions must also be listed in the modules section of the ``iPKG`` file.
|
||||
|
||||
|
||||
For example, lets take the following list of functions that are defined in a module called ``NumOps`` for a sample package ``maths``.
|
||||
|
||||
.. code-block:: idris
|
||||
|
||||
module Maths.NumOps
|
||||
|
||||
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
|
||||
|
||||
.. code-block:: idris
|
||||
|
||||
module Test.NumOps
|
||||
|
||||
import Maths.NumOps
|
||||
|
||||
assertTrue : Eq a => (given : a) -> (expected : a) -> IO ()
|
||||
assertTrue g e = if g == e
|
||||
then putStrLn "Test Passed"
|
||||
else putStrLn "Test failed"
|
||||
|
||||
assertFalse : Eq a => (given : a) -> (expected : a) -> IO ()
|
||||
assertFalse g e = if not (g == e)
|
||||
then putStrLn "Test Passed"
|
||||
else putStrLn "Test failed"
|
||||
|
||||
testDouble : IO ()
|
||||
testDouble = assertTrue (double 2) 4
|
||||
|
||||
testTriple : IO ()
|
||||
testTriple = assertFalse (triple 2) 5
|
||||
|
||||
|
||||
The functions ``assertTrue`` and ``assertFalse`` are used to run expected passing, and expected failing tests.
|
||||
The actual tests are ``testDouble`` and ``testTriple``.
|
||||
These tests are specified in the ``maths.ipkg`` file as follows::
|
||||
|
||||
module maths
|
||||
|
||||
module = Maths.NumOps
|
||||
, Test.NumOps
|
||||
|
||||
tests = Test.NumOps.testDouble
|
||||
, Test.NumOps.testTriple
|
||||
|
||||
|
||||
The testing framework can be innvoked using: ``idris --testpkg maths.ipkg``.
|
||||
Loading…
Reference in New Issue
Block a user