Создавать библиотеку вместо исполняемого файла в Idris?

Есть ли способ генерировать библиотеку вместо исполняемого файла с помощью idris? Если я пытаюсь выполнить компиляцию без main, я получаю такую ​​ошибку:

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

Если я могу сгенерировать библиотеку, тогда есть способ вызвать ее из C-кода? Я посмотрел на сгенерированный код C, но он не выглядит так, как будто он был вызван извне.

Ответы

Ответ 1

Краткая версия, насколько мне известно: по состоянию на октябрь 2015 года:

  • Вы можете создать библиотеку Idris, но не .a или .so.
  • Вы можете позвонить в код C от Idris, но вы не можете позвонить в код Idris с C.

Idris может скомпилировать модуль как библиотеку, но он скомпилирован в файл IBC для связи с другим кодом Idris, а не с объектным файлом .o для связи с C-кодом.

Idris C FFI предназначен для вызова C, а не для вызова в Idris из C. Начиная с октября 2015 года работа продолжается чтобы активировать функции Idris в функции C как указатель функции C, чтобы включить использование API-интерфейсов C на основе обратного вызова.

Пример

В Foo.ipkg:

package Foo

modules = Foo

В Foo.idr:

module Main

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

Строительство:

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

Вы можете увидеть, как создание библиотеки создало два .ibc файла. Если вы хотите создать исполняемый файл вместо этого, вы добавите строки main = … и executable = … в файл .ipkg.