Agda: Unable to do IO - missing Data.FFI, IO.FFI

2
votes

I've done stuff in agda as a hobby for a few months now, and I started to make a provably safe\correct Tic Tac Toe game. I've got all the lemmas proofs and definitions, but now that I have tried to get input and print output I've ran into a problem. All "Hello World" examples taken from the web have failed, most of them with the message that I am missing Data.FFI and IO.FFI. I've looked around for a solution online,, but none were of use. One website said I should run "cabal install" from agda/agda-stdlib-0.11/ffi but I"m not even sure if I have that folder on my computer, and I have many folders named "agda", all over the computer (this is my first time using linux for something, so I probably did stuff horribly) This is the error I get when trying to run the code from EMACS with agda-mode (C-c C-x C-c)

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.

If it matters, I'm running Ubuntu. Thank you very much for the help!

1
iofunctional-programmingagda

1 Answers

3
votes

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

That is correct. From the README for the standard library 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