This repository has been archived by the owner on Jan 5, 2024. It is now read-only.
-
Notifications
You must be signed in to change notification settings - Fork 10
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
- Loading branch information
David Cao
committed
May 3, 2019
1 parent
15be65e
commit 2708ded
Showing
6 changed files
with
210 additions
and
4 deletions.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,203 @@ | ||
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): | ||
|
||
1. Attempt to interpret as a subpath: filename ``pqr.xyz``, extension ``ext`` | ||
1. If there's no file extension or ``ext`` == ``idr`` or ``lidr``: | ||
1. Search for ``a/.../xyz.idr`` | ||
2. Search for ``a/.../xyz.lidr`` | ||
2. Otherwise: | ||
1. Search for ``a/.../xyz.idr``, generate main for fn ``ext`` | ||
2. Search for ``a/.../xyz.lidr``, generate main for fn ``ext`` | ||
3. If either branch failed, continue to next | ||
2. Otherwise, interpret as a mixed or module path: | ||
1. Search for ``$p/a/.../pqr/xyz/ext.idr`` | ||
2. Search for ``$p/a/.../pqr/xyz/ext.lidr`` | ||
3. Search for ``$p/a/.../pqr/xyz.idr``, generate main for fn ``ext`` | ||
(except if ``ext`` == ``idr`` or ``lidr``) | ||
4. 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: | ||
|
||
1. The source path of a subpath is its immediate parent. | ||
2. 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: | ||
|
||
1. ``Tests.idr`` | ||
2. ``tests/Tests/idr.idr`` | ||
3. ``tests/Tests/idr.lidr`` | ||
4. ``tests/Tests.idr`` | ||
5. ``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>`__. |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters