io - Agda:无法执行 IO - 缺少 Data.FFI、IO.FFI

Question

作为一种爱好，我已经在 agda 上做了几个月的事情了，我开始制作一个可证明安全\正确的 Tic Tac Toe 游戏。 我已经获得了所有引理证明和定义，但现在我尝试获取输入和打印输出，但遇到了问题。 所有从网络上获取的“Hello World”示例都失败了，其中大多数都带有我缺少 Data.FFI 和 IO.FFI 的消息。 我在网上寻找了解决方案，但没有一个有用。一个网站说我应该从 agda/agda-stdlib-0.11/ffi 运行“cabal install”，但我什至不确定我的计算机上是否有该文件夹，而且我的计算机上有许多名为“agda”的文件夹(这是我第一次使用 Linux 来做某事，所以我可能做得很糟糕) 这是我尝试使用 agda-mode (C-c C-x C-c) 从 EMACS 运行代码时遇到的错误

Compilation error:

MAlonzo/Code/Agda/Primitive.hs:4:18:
    Could not find module ‘Data.FFI’
    Use -v to see a list of the files searched for.

MAlonzo/Code/Agda/Primitive.hs:5:18:
    Could not find module ‘IO.FFI’
    Use -v to see a list of the files searched for.

如果重要的话，我正在运行 Ubuntu。 非常感谢您的帮助!

Answer 1

One website said I should run "cabal install" from agda/agda-stdlib-0.11/ffi

这是正确的。来自 README对于标准库 0.11:

-- To compile the library using the MAlonzo compiler you first need to
-- install some supporting Haskell code, for instance as follows:
--
--   cd ffi
--   cabal install