shadowhunters - ¿Generar biblioteca en lugar de ejecutable en Idris?

idris shadowhunters

Question

¿Hay una manera de generar una biblioteca en lugar de un ejecutable utilizando idris ? Si intento compilar sin un main , obtengo un error como este:

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

Si puedo generar una biblioteca, ¿hay alguna forma de llamarlo desde el código C? He mirado el código C generado, pero no parece que estuviera destinado a ser llamado externamente.

Answer 1

La versión corta, a mi leal saber y entender: a partir de octubre de 2015:

• Puede generar una biblioteca Idris, pero no una .a o .so.
• Puede llamar al código C desde Idris, pero no puede llamar al código Idris desde C.

Idris puede compilar un módulo como una biblioteca, pero está compilado en un archivo IBC para vincularlo con otro código Idris, no como un archivo objeto .o para vincularlo con el código C.

El C FFI de Idris está destinado a ser usado para llamar a C, no para llamar a Idris desde C. A partir de octubre de 2015, se está trabajando para habilitar la venta de las funciones de Idris a C como un puntero a la función C para habilitar el uso de las API de C basadas en devolución de llamada.

Ejemplo

En Foo.ipkg:

package Foo

modules = Foo

En Foo.idr:

module Main

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

Edificio:

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

Puedes ver cómo la construcción de la biblioteca generó dos archivos .ibc. Si quisiera construir un ejecutable en su lugar, agregaría las líneas main = … y executable = … al archivo .ipkg.