Problems compiling with Agda

2
votes

I installed Adga with 'apt-get install agda-mode'. I've got a working 'Hello World' program written in Agda shown in the screenshot below

enter image description here

But when I go to Agda > Compile it asks me for a 'backend' shown in this second screenshot

enter image description here

I've tried typing in 'GHC' as my back end but it just says '/usr/share/libghc-agda-dev/MAlonzo/src: getDirectoryContents:openDirStream: does not exist (No such file or directory)'

Agda > Load seems to work. How do I get my Agda program to compile?

1
compilationagda
Have you installed agda too? The package agda-mode only provides the emacs mode, not the compiler. – gallais
@gallais, how do I do that? – Adjam

1 Answers

0
votes

I personally recommend you to install agda via haskell's Cabal (you can have it by installing haskell-platform, and installing haskell will install ghc). The debian maintained package of agda is currently broken and has issues with the standard library.

cabal update
cabal install agda

you can install both standard library and agda-mode via apt install. After all that (keep in mind that cabal will compile agda, so it will take some time), add the standard library to agda's local settings. Open emacs and load the file to type-check it, or compile it if it has a executable code.