The Agda developers manual (preliminary version)
Table of contents
Work in progress
Setting up GHCi
To compile Agda in GHCi during development, the CPP macros generated by cabal need to be loaded, otherwise GHCi chokes on some CPP directives. Here is some advice how to pass the options to GHCi: http://stackoverflow.com/questions/19622537/running-ghci-on-a-module-that-needs-language-cpp
In my .emacs file, I (Andreas) have a very brutal setup for the haskell emacs mode to do this for me:
(custom-set-variable '(haskell-program-name "ghci -optP-include -optP/Users/abel/tmp/Agda2/dist/build/autogen/cabal_macros.h +RTS -M1g -RTS") )
If you have a better, more flexible setup, please post it here.