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 includeLightyear.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:
[[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
, extensionext
- If there’s no file extension orext
==idr
orlidr
:- Search for
a/.../xyz.idr
- Search for
a/.../xyz.lidr
- Otherwise:
- Search for
a/.../xyz.idr
, generate main for fnext
- Search fora/.../xyz.lidr
, generate main for fnext
- If either branch failed, continue to next
- Search for
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 fnext
(except if
ext
==idr
orlidr
)- Search for
$p/a/.../pqr/xyz.lidr
, generate main for fnext
(except ifext
==idr
orlidr
)
- Search for
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!)
[[bin]]
path = "src" # also specified by default
main = "Main.idr"
[[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:
[[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
[[bin]]
# We only need files from src/bin
path = "src/bin"
main = "App.Cli.run"
# or main = "App/Cli.run"
[[bin]]
# We only need files from src/bin/App
path = "src/bin/App"
main = "Cli.run"
[[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
:
[[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:
[[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>`__.