mix_idris2

mix_idris2 adds the ability to compile Idris 2 code in a Mix project. The Idris 2 code is compiled to .beam files using the Erlang code generator for Idris 2.

The Erlang code generator for Idris 2 include functions and types to allow interoperability between Idris 2 and Erlang/Elixir. Learn more from its documentation.

Installation

Steps:

1. Add Idris package file
2. Add Idris module
3. Add mix_idris2 as a dependency
4. Update project configuration

1. Add Idris package file

Create a file named hello.ipkg in the same directory as your mix.exs file.

Example package description:

package hello

modules =
  Main

sourcedir = "lib/idris"
builddir = "_build/idris"

library = hello

The modules field should list all Idris modules that are not imported by any other Idris modules. Let's call these for root modules. Root modules commonly include code to export Erlang functions (See example in next section). All Idris modules that are (transitively) imported by a root module will be compiled/generated.

• Documentation about package descriptions

2. Add Idris module

Create a file named Main.idr in the directory lib/idris (same as sourcedir in hello.ipkg).

Example Idris module:

module Main

import Erlang

%cg erlang export exports


hello : String
hello = "Hello from Idris"

exports : ErlExport
exports = Fun "hello" (MkFun0 hello)

This will export the function hello/0 in a module named Elixir.Idris.Main. Note that mix_idris2 will prefix the Idris module names with Elixir.Idris., making them easier to access from Elixir.

3. Add mix_idris2 as a dependency

In your mix.exs, add :mix_idris2 to your list of dependencies:

def deps do
  [
    {:mix_idris2, "~> 0.1.0"}
  ]
end

4. Update project configuration

In your mix.exs, add the keys :idris_ipkg and :compilers to your :project definition.

:idris_options is a keyword list containing the options described in the mix_idris2 options section. The key :idris_options is optional.

Example configuration:

def project do
  [
    idris_ipkg: "hello.ipkg",
    idris_options: [],
    compilers: [:idris] ++ Mix.compilers()
  ]
end

If you are including mix_idris2 in a Phoenix project, the list of compilers should be something like: [:idris, :phoenix, :gettext] ++ Mix.compilers()

Usage

After completing the installation steps, you should be able to call Idris.Main.hello() from an Elixir module. The function call should return the binary: "Hello from Idris"

Learn how to interoperate with Erlang/Elixir from Idris code in the documentation for the Erlang code generator.

mix_idris2 options

The key :idris_options in the :project definition supports the following options:

Option	Default	Description
:executable_path	"idris2erl"	The path to the idris2 executable.
:incremental	false	Enable to only generate code for changed Idris modules. See also: Incremental code generation gotchas
:debug	false	Enable to output additional information in the output.

Example configuration:

def project do
  [
    idris_ipkg: "hello.ipkg",
    idris_options: [executable_path: "idris2erl", incremental: true, debug: true],
    compilers: [:idris] ++ Mix.compilers()
  ]
end

Incremental code generation gotchas

If you want to use the incremental code generation option, you should be aware that mix_idris2 does not currently generate code for all Idris modules that belong to the Idris packages (prelude, base, erlang etc.), only the Idris modules that are referenced in your source code. This means that if you import an Idris module from base that you did not previously reference, the newly imported Idris module will not be generated.

As a workaround you can always run mix compile --force to recompile all the referenced Idris modules.

I want to remove this limitation in the future.

License

mix_idris2 is released under the 3-clause BSD license.