CODEWITHSUNDEEP
idris
mushroom
mushroom

Reputation: 6279

Generate library instead of executable in Idris?

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.

Upvotes: 18

Views: 1558

Answers (1)

Jeremy W. Sherman
Jeremy W. Sherman

Reputation: 36143

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.

Upvotes: 2

Related Questions