Bibliothek generieren statt ausführbar in Idris?

Question

Gibt es eine Möglichkeit, eine Bibliothek anstelle einer ausführbaren Datei mit idris zu generieren? Wenn ich ohne main versuchen kompilieren, ich einen Fehler wie diese:

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

Wenn ich eine Bibliothek erzeugen kann, dann ist es eine Möglichkeit, es zu nennen von C-Code? Ich habe mir den generierten C-Code angesehen, aber es sieht nicht so aus, als ob er extern aufgerufen werden sollte.

Answer 1

Die kurze Version, zum besten meines Wissens: Ab Oktober 2015:

• Sie können eine Idris Bibliothek, aber keine .a erzeugen oder .so.
• Sie können in C-Code aus Idris nennen, aber Sie können in Idris Code von C. nicht nennen

Idris ein Modul als Bibliothek zusammenstellen können, aber es wird mit anderen zu einer IBC-Datei kompiliert für die Verknüpfung Idris-Code, keine O-Objektdatei zum Verknüpfen mit C-Code.

Idris C FFI soll verwendet werden, um in C aufzurufen, nicht in Idris von C abzurufen. Ab Oktober 2015, work is underway zu aktivieren Vending Idris Funktionen zu C als C-Funktionszeiger, um Callback-basierte C-APIs zu ermöglichen .

Beispiel

In Foo.ipkg:

package Foo 

modules = Foo 

In Foo.idr:

module Main 

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

Gebäude:

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

Sie können die Bibliothek erzeugt sehen, wie freundliches Gebäude zwei .ibc-Dateien. Wenn Sie stattdessen eine ausführbare Datei erstellen möchten, fügen Sie der Datei .ipkg main = … und executable = … Zeilen hinzu.