Generate library instead of executable in Idris?

Question

Is there a way to generate a library instead of an executable using idris? If I try compiling without a main, I get an error like this:

main:0:0:When elaborating an application of function run__IO:
    No such variable Main.main

If I can generate a library, then is there a way to call it from C code? I have looked at the generated C code but it doesn't look like it was intended to be called externally.

Answer 1

The short version, to the best of my knowledge: As of October 2015:

• You can generate an Idris library, but not a .a or .so.
• You can call into C code from Idris, but you can't call into Idris code from C.

Idris can compile a module as a library, but it's compiled to an IBC file for linking with other Idris code, not a .o object file for linking with C code.

Idris's C FFI is intended to be used to call into C, not call into Idris from C. As of October 2015, work is underway to enable vending Idris functions to C as a C function pointer to enable using callback-based C APIs.

Example

In Foo.ipkg:

package Foo

modules = Foo

In Foo.idr:

module Main

foo : Int -> Int
foo i = i + 1

Building:

> ls
Foo.idr  Foo.ipkg
> idris --build Foo.ipkg
Type checking ./Foo.idr
> ls
00Foo-idx.ibc Foo.ibc       Foo.idr       Foo.ipkg

You can see how building the library generated two .ibc files. If you wanted to build an executable instead, you would add main = … and executable = … lines to the .ipkg file.