Generowanie biblioteki zamiast wykonywalnych w Idris?

Question

Czy istnieje sposób na wygenerowanie biblioteki zamiast pliku wykonywalnego przy użyciu idris? Gdy próbuję kompilacji bez main, pojawia się błąd jak poniżej:

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

jeśli mogę wygenerować bibliotekę, a następnie czy istnieje sposób aby połączyć go z kodu C? Przyjrzałem się wygenerowanemu kodowi C, ale nie wygląda na to, że miało być nazywane zewnętrznie.

Answer 1

Wersja krótka, do mojej najlepszej wiedzy: Od października 2015:

• Można wygenerować biblioteki Idris, ale nie .a lub .so.
• Można zadzwonić do kodu C z Idris, ale nie możesz zadzwonić do kodu Idris od C

Idris można skompilować moduł jako biblioteka, ale jest skompilowany do pliku IBC do łączenia z innymi Kod idris, a nie plik obiektowy .o do łączenia z kodem C.

Idris c-FFI ma być używany do wywołania w ° C, nie stanie na Idris z C. Od października 2015 work is underway umożliwić automatów funkcji Idris do C jako wskaźnik funkcji C, w celu umożliwienia korzystania zwrotnego opartej C API .

Przykład

W Foo.ipkg:

package Foo 

modules = Foo 

W Foo.idr:

module Main 

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

budynku:

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

można zobaczyć, jak budynek biblioteki generowane dwa pliki .ibc. Jeśli zamiast tego chcesz utworzyć plik wykonywalny, dodaj pliki main = … i executable = … do pliku .ipkg.