Quick Start¶
This section is for getting up-to-speed with elba as fast as possible, covering getting elba installed on your machine in the first place and making a new project.
By the end of this chapter, you should have a basic elba installation up-and-running, as well as a general overview of how to use elba for day-to-day Idris development.
We will assume that you already have the Idris toolchain installed. If you don’t, there are instructions available on the Idris and Blodwen websites.
Installation¶
The easiest and most convenient way of installing elba is to use the
pre-built binaries for elba, which can be downloaded from GitHub
Releases. To install this
way, just download the corresponding archive for your platform, extract
the executable somewhere in your PATH, add ~/.elba/bin
to your PATH
in order to execute elba-installed packages, and you’re done!
Note
For Linux platforms, there are two varieties of binaries available:
one suffixed with -gnu
and the other suffixed with -musl
. The
-gnu
binary is dynamically linked to the system libc, while the
-musl
binary is statically linked using musl.
For most users, the -gnu
binary should work fine, but if it
doesn’t, try using the -musl
binary.
Installing with Cargo¶
Because elba is written in Rust, it is available as an installable crate from crates.io. In order to install elba this way, you should have a copy of the Rust toolchain installed on your computer first. The process for this is explained on the Rust website. The version of of Rust elba has successfully been built on is nightly-2020-02-21.
Once you have Rust installed, installing elba is self-explanatory:
$ cargo install elba
$ elba # should work
Remember to add ~/.elba/bin
to your PATH to be able to run
elba-installed packages.
Building elba¶
Building elba from source is much the same process as installing it using cargo; the only difference is that instead of using a stable, versioned-crate available from crates.io, elba’s source code is used directly. You’ll still need to have Rust 1.31 or later installed. After that’s done, download elba’s source code and install it:
$ git clone https://github.com/elba/elba
$ cd elba
$ cargo install --path .
$ elba # should work!
Remember to add ~/.elba/bin
to your PATH to be able to run
elba-installed packages.
Creating a package¶
Creating a package is easy with elba: all you need is a package name. Note that names in elba are special in that they are always namespaced; every name in elba comes with a group part and a name part, separated with a slash. For more information, see the information on names in the manifest chapter.
$ elba new asd # won't work: no namespace
$ elba new grp/asd # ok!
This command will generate a new elba project with name grp/asd
in
the folder ./asd/
, along with an associated git project. If you want
to omit the git project, pass the option --vcs none
.
By default, elba will create a project with a binary target, with a main
file located at src/Main.idr
. If you’d like to generate a package
with a library target instead, pass the --lib
flag, which will add a
library target to the manifest and generate the file
src/{group}/{name}.idr
. This file structure of having a group
followed by a name is just convention, and isn’t required.
Regardless of which target is chosen, an elba.toml
manifest file
will also be generated.
Initializing a pre-existing package¶
If you already have an Idris project and want to turn it into an elba
project, use the elba init
command instead; it follows the exact
same syntax as elba new
and is functionally identical, but uses the
current directory instead of making a new one.
Adding dependencies¶
Now that a new package has been created, you can start to add packages
as part of your dependencies. A package can originate from one of three
places: a git repository, a file directory, or a package index. Ordinary
dependencies are placed under the [dependencies]
section, while
dependencies that are only needed for tests and the like are placed
under [dev_dependencies]
. Examples are shown below:
[dependencies]
"index/version" = "0.1.5" # uses the default index (i.e. the first specified one in configuration)
"index/explicit" = { version = "0.1.5", index = "index+dir+../index" } # uses the index specified
"directory/only" = { path = "../awesome" } # uses the package in the path specified
"git/master" = { git = "https://github.com/doesnt/exist" } # uses the master branch
"git/explicit" = { git = "https://github.com/doesnt/exist", tag = "beta" } # "tag" can be an arbitrary git ref: a branch, a tag, commit, etc.
For more information on the syntax regarding specifying and adding custom indices, see the chapters on Resolutions and ../usage/configuration. More information about dependency specification syntax is available at its relevant chapter.
Note that only packages with library targets can be depended on.
At this point, you can add whatever files you want and import anything from your dependencies.
Targets¶
The manifest also allows you to specify which targets you want to have built for your package. There are three types of targets:
A library target allows this package to be depended on by other packages. A package can only have one library, and the syntax follows the following:
[targets.lib] # the path which contains all of the lib files (*cannot* be a parent directory) # this is set to "src" by default path = "src/" # a list of files to export mods = [ "Awesome.A", # the file src/Awesome/A.idr "Control.Zygohistomorphic.Prepromorphisms", # the file src/Control/Zygohistomorphic/Prepromorphisms.idr ]
A bin target specifies a binary to be built. Multiple binaries can correspond to one package.
[[targets.bin]] # the name of the binary to create name = "awes" # the path which contains all of the bin files (*cannot* be a parent directory) # this is set to "src" by default path = "src/" # the path to the Main module of the binary main = "Awesome.B"
Note: the format of the binary target has some nuance to it, so for more information, see the docs on the manifest format.
A test target specifies a test binary to build. It uses the same syntax as a bin target, with the difference that we use
[[targets.test]]
to specify them and the test binary can depend on the dev-dependencies as well as the root package’s library. A test binary succeeds upon execution if it returns exit code 0.
Building a package¶
…can be accomplished with the command:
$ # assuming the current directory is an elba package
$ elba build
For all elba build-related commands, the IDRIS_OPTS
environment
variable will dictate additional arguments to pass to the Idris compiler
(the flags passed by elba get higher priority). Additionally, any args
passed after a double-dash will be interpreted as arguments to the
Idris compiler:
$ # adds both the contrib and effects built-in packages
$ IDRIS_OPTS="-p contrib" elba build -- -p effects
When building a local package, the output binaries are located at
target/bin
, while the output library is placed at target/lib
.
Interactive development with the REPL can also be accomplished with the command:
$ # assuming the current directory is an elba package
$ elba repl
Instead of placing the build outputs in a target/
folder, the
elba repl
command directly loads the files on-disk, then cleans up
any build files after execution.
elba uses an elba.lock
lockfile to ensure that these builds are
reproducible. This should be committed to repositories for libraries,
but not for binaries.