在Idris中生成库而不是可执行文件？

Question

有没有办法生成库而不是使用可执行文件idris？如果我尝试编译没有a main,我得到这样的错误:

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

如果我可以生成一个库,那么有没有办法从C代码调用它？我已经查看了生成的C代码,但它看起来并不打算在外部调用.

Answer 1

据我所知，简短版本：截至 2015 年 10 月：

\n\n

\n
• 您可以生成 Idris 库，但不能生成 .a 或 .so。
\n
• 您可以从 Idris 调用 C 代码，但不能从 C 调用 Idris 代码。
\n

\n\n

Idris 可以将模块编译为库，但它被编译为 IBC 文件以与其他 Idris 代码链接，而不是编译为 .o 目标文件以与 C 代码链接。

\n\n

Idris 的 C FFI 旨在用于调用 C，而不是从 C 调用 Idris。截至 2015 年 10 月，我们正在努力将 Idris 函数作为 C 函数指针出售给 C，以便能够使用基于回调的 C蜜蜂。

\n\n

例子

\n\n

在 Foo.ipkg 中：

\n\n

package Foo\n\nmodules = Foo\n

\n\n

在 Foo.idr 中：

\n\n

module Main\n\nfoo : Int -> Int\nfoo i = i + 1\n

\n\n

建筑：

\n\n

> ls\nFoo.idr  Foo.ipkg\n> idris --build Foo.ipkg\nType checking ./Foo.idr\n> ls\n00Foo-idx.ibc Foo.ibc       Foo.idr       Foo.ipkg\n

\n\n

您可以看到构建库如何生成两个 .ibc 文件。如果您想构建可执行文件，则可以将main = \xe2\x80\xa6和 行添加executable = \xe2\x80\xa6到 .ipkg 文件中。

\n