The 13th episode of Ivor the Engine (in colour) is titled Unidentified Objects. Let's hope our codebase don't have any of those.
Idris the Dragon
- Idris rules for Bazel
- Table of Contents
- Overview
- Getting Started
- Add rules_idris to a bazel project
- Tutorials
- Known Issues
- Other Idris build tools / package managers
- Roadmap
ToC created by gh-md-toc
Idris rules adds Idris support for Bazel. Bazel is a powerful and well maintained build tool with a lot of interesting characteristics. Combining Bazel and idris rules, we get an idris build tool that:
- Can build different types of components (executables, libraries and tests)
- Make components easy to integrate between them
- It's easy to configure (for example, there is no need to specify the list of files/modules of your component by hand)
- Supports external dependencies. External dependencies only need to be Idris+Bazel projects hosted somewhere (like github, bitbucket, gitlab, ...). This means that, to support external dependencies there is no need to create and maintain some kind of central repository infrastructure. And it's easy for library developers to publish their work.
And there are more features to come
PREREQUISITES: Having bazel installed locally
Two quick options to get you started:
-
If you are already familiar with bazel, you can continue with the add rules_idris to a bazel project section
-
Otherwise head to the create a simple hello world tutorial
To get started with rules_idris, you only need to initialize them on your WORKSPACE
file and you will be ready to go. For that you have two options:
-
If you have the nix package manager installed locally, you can use it and bazel is going to get idris for you.
-
Otherwise, you can use a local installation of idris
Afterwards you might want to add an executable, a module or a test
PREREQUISITES: Having nix installed locally
This approach allows nix to retrieve idris for you. In fact, in the future this will allow per project configuration of the idris version to use.
Add the following to your WORKSPACE
file:
load("@bazel_tools//tools/build_defs/repo:git.bzl", "git_repository")
git_repository(
name = "rules_idris",
remote = "https://github.com/BryghtWords/rules_idris.git",
tag = "v0.3"
)
load("@rules_idris//idris:idris_repos.bzl", "loadIdrisRepositories")
loadIdrisRepositories()
load("@rules_idris//idris:idris_loader.bzl", "loadIdris")
loadIdris()
PREREQUISITES: Having idris installed locally
With this approach, you need a local installation of idris, and to tell bazel where to find it.
- Add the following snippet into your
WORKSPACE
file
load("@bazel_tools//tools/build_defs/repo:git.bzl", "git_repository")
git_repository(
name = "rules_idris",
remote = "https://github.com/BryghtWords/rules_idris.git",
tag = "v0.3"
)
load("@rules_idris//idris:idris_repos.bzl", "loadIdrisPackagerRepositories")
loadIdrisPackagerRepositories()
load("@rules_idris//idris:local_idris_loader.bzl", "loadIdris")
loadIdris("/path/to/idris/installation") # That is, wichever path that contains 'bin/idris'
- Locate where you have idris installed (that is, the folder that contains
bin/idris
) - On the text you have just added, replace
/path/to/idris/installation
with the correct path
Add the following into the BUILD
file for your executable:
load("@rules_idris//idris:rules_idris.bzl", "idris_binary")
idris_binary (
name = "name_of_the_binary",
)
It will automatically pick up all the idr
files from the same folder than the BUILD
file
Add the following into the BUILD
file for your module:
load("@rules_idris//idris:rules_idris.bzl", "idris_library")
idris_library (
name = "name_of_the_library",
visibility = ["//visibility:public"],
)
It will automatically pick up all the idr
files from the same folder than the BUILD
file
If we want to test a library, like the one from the previous section, we should tweak it's BUILD
file to look like this:
load("@rules_idris//idris:rules_idris.bzl", "idris_library", "idris_test")
idris_library (
name = "library_example",
visibility = ["//visibility:public"],
)
idris_test (
name = "test_example",
deps = ["library_example"],
)
The idris_test
rule is going to pick up all the idr
files from the test
subfolder from where the BUILD
file is located. Each idr
in the test should have a test method with this signature:
export
test : IO Bool -- This should be true if the test or tests in this suite are successful
The implementation of this method should return true if all the tests of this suite pass, or false otherwise. This will allow for easy integration with external testing libraries.
Creating a basic project for a simple executable, is a simple three step process:
- Create the project
- Setup idris rules
- Add the executable module
Bazel projects (also called workspaces) are collections of targets. For simplicity, I'm going to say that targets are things that can be built (this is not really true, but will help understand how bazel works).
In turn, this targets are organized into packages. All targets must belong to a package.
You can think of a workspace as a folder that contains a file named WORKSPACE
. Everything in that folder and subfolders belong to the workspace. Likewise, the WORKSPACE
file must live in the root folder of your project.
You can think of a package as a folder in the workspace that contains a file named BUILD
. Everything in that folder and subfolders that are not packages themselves (that is, that don't contain a BUILD
file) belong to the package.
If you look at this example:
|____my-package
| |____BUILD
| |____foo.h
| |____src
| | |____bar.cpp
| |____sub
| | |____BUILD
| | |____baz.h
| | |____src
| | | |____qux.cpp
my-package/foo.h
and my-package/src/bar.cpp
belong to the package my-package
, where my-package/sub/baz.h
and my-package/sub/src/qux.cpp
belong to sub
It's also worth noticing that the root folder can be both the workspace and a package. That is, by containing both a WORKSPACE
file and a BUILD
file.
The WORKSPACE
file holds general configuration for the project, things like what external repositories to access or tools to use. The BUILD
files list the targets for that package.
A bazel project is just a folder with a WORKSPACE
file. Here we go:
mkdir my-project
cd my-project
touch WORKSPACE
On this step you have to choose:
- To use the nix package manager (and install it if you don't already have it)
or
- To use a local installation of idris (and install it if you don't already have it)
After that, you basically need to add content on your WORKSPACE
file to tell bazel how to get and use rules_idris. It's preatty much a copy-and-paste as explained in here if you use nix or, otherwise as explained in here if you use a local installation of idris
This is where we create our first bit of idris. We will do three things:
- Create the package
- Create the idris code
- Configure the target
So first, as mentioned before, a package is a folder with a BUILD
file. Starting from the root folder:
mkdir bin # we can name this folder whatever we want
cd bin
touch BUILD
Then we need a bit of idris code. Let's put this code in bin/Binary.idr
:
module Main
main : IO ()
main = putStrLn "Hello, world!"
And finally, we need to tell bazel about it. Let's add this to the bin/BUILD
file:
load("@rules_idris//idris:rules_idris.bzl", "idris_binary")
idris_binary (
name = "binary_example",
)
And that's it, we can now build it:
bazel build //bin:binary_example
Or run it:
bazel run //bin:binary_example
After running either command, you can find your new file at:
bazel-bin/bin/bin/binary_example
You can open the idris repl with all the dependencies (external or otherwise) in scope. For example, if we want to play with the code from the previous tutorial, just run this:
bazel run //bin:binary_example_repl
To opend the repl for a module, there is an special module created for every idris rule that starts the repl. This module is named exactly like the rule, with "_repl" added at the end.
Call it module or library, the distinction is quite difuse in bazel. What we are talking about is a bunch of reusable code that is not, by itself, an executable. For that, all we need is a target that describes how to create this module. And usualy, we put modules on their own packages.
This tutorial follows up from create a simple hello world, so from the root folder from the result of that tutorial, we are going to do the following:
- Create a package and module
- Implement some functionality for the module
- Make our binary use the module
We only need a new folder and BUILD
file:
mkdir lib
touch lib/BUILD
And tell the BUILD
file about our new module. Write this into the BUILD
file:
load("@rules_idris//idris:rules_idris.bzl", "idris_library") # This puts the `idris_library` function in scope. It's basically an `import`
# This declares the new library
idris_library (
name = "salutes", # Named `salutes`
visibility = ["//visibility:public"], # Accessible from any other bazel target
)
Let's start wit a simple bit of idris code. Create the file lib/Salute.idr
, and add it's functionality:
module lib.Salute
export
salute : String
salute = "Hello, library example of idris"
Two steps, first tell the binary target it can use the new module. Fot that, edit bin/BUILD
to make it look like this:
load("@rules_idris//idris:rules_idris.bzl", "idris_binary")
idris_binary (
name = "binary_example",
deps = ["//lib:salutes"], # This is the line that has been added
)
And finally, let's make un application use the library. Edit bin/Binary.idr
, to use the new function:
module Main
import lib.Salute
main : IO ()
main = putStrLn salute
You can try your new code as explained in here.
From the point of view of bazel, a test is an executable that once run its exit status id either 0 when everything has gone ok or not 0 if something has gone wrong. Bazel doesn't care for anything else.
For this purpose, idris rules provides idris_test
. A rule that generates the executable's main
function for you. And expects a single test
function on each source file on the test module. This test
functions must have this signature:
export
test : IO Bool -- This should be true if the test or tests in this suite are successful
Given that, only idris_library
modules can be tested because the test itself must be an executable and merging two executables is dificult.
So, for this tutorial we are going to start from the result of create a simple module.
Tests live on the test
subfolder of the module you want to test. Since we are testing the lib:salutes
module, from the root folder execute:
mkdir lib/test
touch lib/test/SaluteTest.idr
And write a simple test on lib/test/SaluteTest.idr
:
module lib.test.LibTest
import lib.Library
export
test : IO Bool
test = pure (salute == "Hello, library example of idris")
Now, we only need to register the new test module. For that purpose, edit lib/BUILD
to look like this:
load("@rules_idris//idris:rules_idris.bzl", "idris_library", "idris_test") # CHANGE 1: This now also imports `idris_test`
idris_library (
name = "salutes",
visibility = ["//visibility:public"],
)
# CHANGE 2: Add the new test module
idris_test (
name = "test_salutes",
deps = ["salutes"], # This tells bazel to link the library we are testing into the executable that is going to run the tests
)
And that's it, we can now build our testing module:
bazel build //lib:test_salutes
Or run the tests directly:
bazel test //lib:test_salutes
NOTE: By default, bazel logs the result of running the tests but doesn't print them on STDOUT. If you want to see the results of running the test (which since there is no putStrLn
is going to be empty anyway), you should run this:
bazel test //lib:test_salutes --test_output=all
To make one of your modules use an external library, you need to a) declare it on your WORKSPACE file and b) make the module depend on it.
So, imagine we want to improve our tests from the previous tutorial. And for that, we want to make use of IdirsTest, an external library.
We will start this tutorial from the result of the write a simple idris test tutorial.
First, we need to make our project aware of the external dependency. For that we need to add this to our WORKSPACE
file:
git_repository(
name = "IdrisTest",
remote = "https://github.com/BryghtWords/IdrisTest.git",
tag = "v0.1"
)
Second, we need to tell our module (in this case, our test) that it can use the external dependency. Let's modify lib/BUILD
:
load("@rules_idris//idris:rules_idris.bzl", "idris_library", "idris_test")
idris_library (
name = "salutes",
visibility = ["//visibility:public"],
)
idris_test (
name = "test_salutes",
deps = [
"salutes",
"@IdrisTest//idristest:idristest", # CHANGE: This tells bazel that `test_salutes` should
# depend on the `idristest` library from the
# `idristest` package in the `IdrisTest` repo.
],
)
Finally, we can use the testing library to improve our test. Let's change our lib/test/SaluteTest.idr
:
module lib.test.LibTest
import lib.Library
import idristest.Suite -- CHANGE 1: Import the tools from the IdrisTest
-- CHANGE 2: Add one unit test
testLibrary1 : (Bool, String)
testLibrary1 = assertEq
"Test salute" -- Test title
salute -- Result
"Hello, library example of idris" -- Expected
-- CHANGE 3: Add another unit test
testLibrary2 : (Bool, String)
testLibrary2 = assertNotEq
"Test salute diff" -- Test title
salute -- Result
"Ups" -- Expected to be different
-- CHANGE 3: The main test function aggregates all the other tests
export
test : IO Bool
test = runTests [testLibrary1, testLibrary2]
Now you can run your test in the same way as explained in how to run your tests
Briefly: an external library is a bazel project whose source code lives on github (or similar). More specificaly a bazel project that can be git clone
ed.
Let's imagine we want to publish our salutes library available for the world to use. We need to create the scaffolding:
mkdir salutes
cd salutes
touch WORKSPACE
Now we need to install idris rules as explained on add rules_idris to a bazel project
We are going to place our library in the lib
folder:
mkdir lib
touch lib/BUILD
touch lib/Salute.idr
where we are goint to have a lib/BUILD
like this:
load("@rules_idris//idris:rules_idris.bzl", "idris_library") # This puts the `idris_library` function in scope. It's basically an `import`
# This declares the new library
idris_library (
name = "salutes", # Named `salutes`
visibility = ["//visibility:public"], # Accessible from any other bazel target
)
and a lib/Salute.idr
similar to this:
module lib.Salute
export
salute : String
salute = "Hello, library example of idris"
Now, create a repository on your site of choise (github/bitbucket/...) and push the content of your new library. As simple as that.
It's usualy a good idea to let your users know how to import your library. For that, a good approach is to write an snippet similar to this in your README
file:
To import `salutes` into your project, you need to add this block into your `WORKSPACE` file:
```python
git_repository(
name = "salutes",
remote = "https://github.com/<my_github_username>/<repo_name>.git",
tag = "<tag_of_the_release_to_use>"
)
```
The remote
field should have whatever URL is needed to clone the project. The tag
field can be replaced by a commit
field with the commit id to be used.
- Testing of the rules themselves needs to be improved. In the examples folder there is a prety big collection of bazel projects using rules_idris, with a different organisation each. And there is a 'test' script that builds and runs each of them in turn ensuring that everything goes well, but proper unit testing would be in order.
- Ikan - A package manager for idris, in idris
- Elba - A package manager for Idris
- idream - A simple build system for Idris
- Improve testing integration
- Add support for starting the idris console from bazel
- Add support for the IDE mode on bazel projects
- Support multiple idris versions
- Add javascript and jvm rules
- Migrate the companion IdrisPackager project from Scala to Idris
- Improve reporting of test results