Idris FFI“未找到符号”

Question

我最近一直在尝试使用Idris，并决定尝试使用它的Network.Socket库。我启动了REPL，导入了模块，并使用socket命令创建了一个套接字。在尝试执行IO操作时，遇到以下错误：

failed to construct ffun from (Builtins.MkPair (FFI_C.C_Types (Int)) (Int) (FFI_C.C_IntT (Int) (FFI_C.C_IntNative)) (2),Builtins.MkPair (FFI_C.C_Types (Int)) (Int) (FFI_C.C_IntT (Int) (FFI_C.C_IntNative)) (1),[])
Symbol "socket" not found
user error (Could not call foreign function "socket" with args [2,1,0])

为了查看这个问题是Network.Socket特有的，还是一般的FFI，我做了一个伪函数。

printf : String -> IO ()
printf = foreign FFI_C "printf" (String -> IO ())

执行的:x printf "Hello World"会产生类似的错误：

Symbol "printf" not found
user error (Could not call foreign function "printf" with args ["hello world"])

尽管如此，putStr仍然工作得很好。

我运行的是Idris9.20，它是通过cabal安装的，在编译时设置了-f FFI。我使用的是通过MacPorts安装的libffi3.4版本。

Answer 1

我认为这与Idris FFI的操作方式不同有关，这取决于代码是被编译还是被解释。在编译代码时，FFI要求在C代码生成阶段，命名的C函数在作用域中，并且在链接C可执行文件时，要链接正确的名称。由于Idris的RTS链接到libc，这使得来自libc的许多名称无需任何额外的工作(某些名称可能需要%include来确保包含正确的C头文件以将其放入作用域中)。解释代码时，解释器在动态加载的库列表中查找FFI调用，这需要不同的指令:文件中的%dynamic或解释器中的:dynamic。默认情况下，不加载动态库，因此即使是libc中的标准名称也不在作用域内。这可以通过在文件中包含%dynamic "libc"或者在一个会话的REPL命令行中使用:dynamic "libc"来解决。