Binaries and Tests
==================
Although specifying a library target is pretty straightforward, trying
to get a binary or a test target working can involve a lot more
finagling; elba supports multiple syntaxes and ways to specify a
binary target (and by extension, a test target, since test targets are
just spruced-up binary targets under-the-hood) in order to ensure
maximum flexibility and compatibility with the existing Idris code out
in the wild. Although there is information about these kinds of targets
:doc:`in the reference <../reference/manifest>`__, this section will
help you build some intuition as to the building blocks of the binary
target specification system, and will provide a "cookbook" of common
usecases to follow.
Terminology
-----------
There are a few terms you should know as a prerequisite:
- A **subpath** is a subdirectory of the project's root folder. By
definition, subpaths cannot refer to parent or absolute directories.
Examples include ``bin/``, ``bin/Whatever/Module``, ``Lightyear.idr``,
etc.
- A **module path** is the ``A.B.C`` name associated with a given Idris
file ("module"). Names in the module path are separated with periods,
and their precise location is determined by other config keys in the
manifest. Examples include ``Lightyear.Core``,
``Control.Monad.Tardis``, etc.
Subpaths and module paths can actually be combined into a **mixed path**,
like in ``src/Lightyear.Core`` or ``tests/one/Tests.Unit.API``. The
parts which are separated with slashes are considered the subpath
portion (``src``, ``tests/one``), while the parts separated with periods
are the module portion (``Lightyear.Core``, ``Tests.Unit.API**). When
mixed, subpaths always precede module paths. These types of strings--
subpaths, module paths, or mixed paths--will be referred to as
**target strings** or **target specifiers**.
In order to account for main functions which aren't named ``Main.main``,
elba allows for generation of a main file which points to a function
in another module. This will be referred to as "generating a main file"
for another function.
Resolution Rules
----------------
There are multiple components to any binary or test target; for our
purposes, the relevant parts are the ``path`` and ``main`` specifiers.
``main`` is required and refers to a target string, while ``path``
refers to a parent directory in which the target string should be
searched for. ``path`` can be omitted: its default value is ``src/``
for binary targets and ``tests/`` for test targets.
Given the following binary target:
.. code-block:: toml
[[bin]]
path = "$p"
main = "a/.../pqr.xyz.ext"
elba will go through the following rules to resolve a target specifier
(the first search which works is used):
- Attempt to interpret as a subpath: filename ``pqr.xyz``, extension ``ext``
- If there's no file extension or ``ext`` == ``idr`` or ``lidr``:
- Search for ``a/.../xyz.idr``
- Search for ``a/.../xyz.lidr``
- Otherwise:
- Search for ``a/.../xyz.idr``, generate main for fn ``ext``
- Search for ``a/.../xyz.lidr``, generate main for fn ``ext``
- If either branch failed, continue to next
- Otherwise, interpret as a mixed or module path:
- Search for ``$p/a/.../pqr/xyz/ext.idr``
- Search for ``$p/a/.../pqr/xyz/ext.lidr``
- Search for ``$p/a/.../pqr/xyz.idr``, generate main for fn ``ext``
(except if ``ext`` == ``idr`` or ``lidr``)
- Search for ``$p/a/.../pqr/xyz.lidr``, generate main for fn ``ext``
(except if ``ext`` == ``idr`` or ``lidr``)
These rules make more sense in practice.
Source & Target Paths
---------------------
Internally, elba splits a path into two parts: a **source path** and a
**target path**. Any file which is located in the source path will be
included in the Idris build invocation with the ``--include`` flag (i.e.
your source files *will not* be available unless they are located under
the source path). To determine where to divide the source and target
paths, elba uses the following rules:
- The source path of a subpath is its immediate parent.
- The source path of a mixed or module path is the value of the
``path`` specifier.
In Practice
-----------
This section contains a few handy examples of common patterns for
target specifiers.
Files in src/ directory
~~~~~~~~~~~~~~~~~~~~~~~
Let's say your project has a file ``src/Main.idr``, with a function
``Main.main``. You could generate a binary for it in the following
ways (don't use all the ``[[bin]]`` blocks at once!)
.. code-block:: toml
[[bin]]
path = "src" # also specified by default
main = "Main.idr"
.. code-block:: toml
[[bin]]
# this is a subpath, so path will be ignored:
main = "src/Main.idr"
src/ directory, custom main
~~~~~~~~~~~~~~~~~~~~~~~~~~~
Now, let's say you decide to move your main file to somewhere more
exotic, like ``src/bin/App/Cli.idr``, with a main function
``App.Cli.run``. Which bin target you use depends on which files your
binary will need to import to work:
.. code-block:: toml
[[bin]]
# This binary needs files from the `src` directory
# This line is the default, so it isn't necessary
path = "src/"
main = "bin/App.Cli.run"
# this works as long as the file "bin/App.Cli.idr" doesn't exist
# also works: main = "bin/App/Cli.run", so long as
# "bin/App/Cli/run.idr" doesn't exist
.. code-block:: toml
[[bin]]
# We only need files from src/bin
path = "src/bin"
main = "App.Cli.run"
# or main = "App/Cli.run"
.. code-block:: toml
[[bin]]
# We only need files from src/bin/App
path = "src/bin/App"
main = "Cli.run"
.. code-block:: toml
[[bin]]
# Equivalent to above
# Whatever we set path to is irrelevant; elba will resolve main as a
# subpath first
main = "src/bin/App/Cli.run"
Adding a test
~~~~~~~~~~~~~
Because tests and binaries are represented the same way to elba, the
same rules and processes apply here too. Let's add a test function
``runTests`` in the file ``tests/Tests.idr``:
.. code-block:: toml
[[test]]
path = "tests"
main = "Tests.runTests"
``.idr`` and ``.lidr``
~~~~~~~~~~~~~~~~~~~~~~~~~~
elba has special cases for target specifiers that end in ``idr`` or
``lidr``. If you add a test target like so:
.. code-block:: toml
[[test]]
path = "tests"
main = "Tests.idr"
elba will look for:
- ``Tests.idr``
- ``tests/Tests/idr.idr``
- ``tests/Tests/idr.lidr``
- ``tests/Tests.idr``
- ``tests/Tests.lidr``
elba will never try to generate anything if the target specifier ends
with ``.idr`` or ``.lidr``.
More examples of these are available in :doc:`the reference
<../reference/manifest>`__.