Skip to content

Latest commit

 

History

History
288 lines (188 loc) · 10.1 KB

README.md

File metadata and controls

288 lines (188 loc) · 10.1 KB
Raw

Idris rules for Bazel

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

Overview

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

Getting Started

PREREQUISITES: Having bazel installed locally

Two quick options to get you started:

Add rules_idris to a bazel project

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:

Afterwards you might want to add an executable, a module or a test

Install idris_rules using nix

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.1"
)

load("@rules_idris//idris:idris_repos.bzl", "loadIdrisRepositories")

loadIdrisRepositories()

load("@rules_idris//idris:idris_loader.bzl", "loadIdris")

loadIdris()

Install idris_rules using a local idris installation

PREREQUISITES: Having idris installed locally

With this approach, you need a local installation of idris, and to tell bazel where to find it.

  1. 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.1"
)

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'
  1. Locate where you have idris installed (that is, the folder that contains bin/idris)
  2. On the text you have just added, replace /path/to/idris/installation with the correct path

Create an idris executable

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

Create an idris module

Add the following into the BUILD file for your executable:

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

Test an idris module

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 ()

And the implementation of that method should do nothing if all the tests pass, or exit with a non zero value if the test fails. This will allow for easy integration with external testing libraries.

Tutorials

Create a simple hello world

Creating a basic project for a simple executable, is a simple three step process:

  1. Create the project
  2. Setup idris rules
  3. Add the executable module

Concerning Bazel

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.

1. Create the project

A bazel project is just a folder with a WORKSPACE file. Here we go:

mkdir my-project
cd my-project
touch WORKSPACE

2. Setup rules_idris

On this step you have to choose:

  1. To use the nix package manager (and install it if you don't already have it)

or

  1. 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

3. Add the executable module

This is where we create our first bit of idris. We will do three things:

  1. Create the package
  2. Create the idris code
  3. 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",
)

Let's try it

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

Known Issues

  • Testing integration needs to be improved:
    • Each test component is a collection of Idris modules that contain a test function, if any of this test functions fail, the rest of test functions of that component will not get executed.
    • Right now, the tests get executed in the bazel build fase. Idiomatic bazel requires that to happen in the run fase.
  • Testing of the rules themselves need to be improved. In the examples foldere 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. And also integrate a CI so that we can have automatic checks that everything works.

Roadmap

  • 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