代码之家 › 专栏 › 技术社区 › Adi Ostrov

Agda:无法执行IO-数据丢失。海外金融机构,IO。外国金融机构

agda functional-programming io

2

Adi Ostrov · 技术社区 · 8 年前

我在agda做了几个月的业余爱好,我开始制作一款安全的井字游戏。我已经得到了所有引理的证明和定义,但现在我试图获得输入和打印输出,我遇到了一个问题。我在网上四处寻找解决方案,但都没有用。一个网站说我应该从agda/agda-stdlib-0.11/ffi运行“cabal安装”,但我甚至不确定我的电脑上是否有那个文件夹,我有很多名为“agda”的文件夹,遍布电脑(这是我第一次使用linux做某事,所以我可能做得很糟糕)

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.

非常感谢您的帮助!

1 回复 | 直到 8 年前

1

3

asr 8 年前

一个网站说我应该从agda/agda-stdlib-0.11/ffi运行“阴谋集团安装”

这是正确的。从 README 对于标准库

-- 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