TOC

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.

Syntax

1. Overview

Bug fixing

1. Andreas' notes from several bugfixing tutorials