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.


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:

path = "$p"
main = "a/.../"

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, 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!)

path = "src" # also specified by default
main = "Main.idr"
# 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 Which bin target you use depends on which files your binary will need to import to work:

# This binary needs files from the `src` directory
# This line is the default, so it isn't necessary
path = "src/"
main = "bin/"
# this works as long as the file "bin/App.Cli.idr" doesn't exist
# also works: main = "bin/App/", so long as
# "bin/App/Cli/run.idr" doesn't exist
# We only need files from src/bin
path = "src/bin"
main = ""
# or main = "App/"
# We only need files from src/bin/App
path = "src/bin/App"
main = ""
# Equivalent to above
# Whatever we set path to is irrelevant; elba will resolve main as a
# subpath first
main = "src/bin/App/"

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:

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:

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>`__.