CODEWITHSUNDEEP
compilationagda
Adjam
Adjam

Reputation: 640

Problems compiling with Agda

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?

Upvotes: 2

Views: 1018

Answers (1)

Maycon Amaro
Maycon Amaro

Reputation: 9

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.

Upvotes: 0

Related Questions