Tạo thư viện thay vì thực thi trong Idris?

Question

Có cách nào để tạo thư viện thay vì tệp thực thi bằng cách sử dụng idris không? Nếu tôi cố gắng biên soạn mà không có một main, tôi nhận được một lỗi như thế này:

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

Nếu tôi có thể tạo ra một thư viện, sau đó là có một cách để gọi nó từ mã C? Tôi đã nhìn vào mã C được tạo ra nhưng nó không giống như nó được dự định được gọi là bên ngoài.

Answer 1

Phiên bản ngắn, với tất cả sự hiểu biết của tôi: Tính đến tháng 10 năm 2015:

• Bạn có thể tạo một thư viện Idris, nhưng không phải là một .a hoặc .so.
• Bạn có thể gọi vào mã C từ Idris, nhưng bạn không thể gọi vào mã Idris từ C.

Idris có thể biên dịch một module như thư viện, nhưng nó được biên dịch vào một tập tin IBC để liên kết với khác Mã Idris, không phải là tệp đối tượng .o để liên kết với mã C.

FRI của Idris được dự định sẽ được sử dụng để gọi vào C, không gọi vào Idris từ C. Tính đến tháng 10 năm 2015, work is underway để bật chức năng Idris tự động đến C dưới dạng con trỏ hàm C để bật sử dụng API C dựa trên cuộc gọi .

Ví dụ

Trong Foo.ipkg:

package Foo 

modules = Foo 

Trong Foo.idr:

module Main 

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

xây dựng:

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

Bạn có thể thấy tòa nhà có các thư viện tạo hai tệp .ibc. Nếu bạn muốn xây dựng một tệp thi hành thay vào đó, bạn sẽ thêm các dòng main = … và executable = … vào tệp .ipkg.