[Agda] During and after the Agda installation

[Gyesik Lee]

Hi,

I am sorry, but I have to bother you again.

With the help of many people, I could finish the preparation of the
Agda installation.
But I could not still use Agda on my macbook.

I need more your help.

1. during the installation, I followed the instruction as follows:

 runhaskell Setup.hs configure --user --prefix=~/agda2/
 runhaskell Setup.hs build
 sudo runhaskell Setup.hs install

And the final step finished with the following messages:

Installing library in /Users/leegy/agda2/lib/Agda-2.1.3/ghc-6.10.1
Registering Agda-2.1.3...
Reading package info from "dist/installed-pkg-config" ... done.
Writing new package config file... done.

It looks fine although the messages are a little bit too short.
In the installed directory  '~/agda2/ I can find just  'lib' and
'share' folders.

Does it mean the installation worked well?

2. Anyway, I then followed the instruction further to customize the
emacs (and Aquamacs both.)
and put the following lines in the .emacs (and in the customization.el
for aquamacs.)

(add-to-list 'load-path
"/opt/local/var/macports/sources/rsync.macports.org/release/ports/lang/")
     (<- here is the haskell-mode.el)
(add-to-list 'load-path "/Applications/Aquamacs
Emacs.app/Contents/Resources/site-lisp/edit-modes/haskell-mode/")
(add-to-list 'load-path "/Applications/Aquamacs
Emacs.app/Contents/Resources/site-lisp/edit-modes/agda-mode/")     (<-
here are the agda-mode files, copied from  ..../emacs-mode/ in the
source files.)
(require 'agda2)


But during the start-up of emacs, one error message came up:

File mode specification error: (error "Required feature `haskell-ghci'
was not provided")

Emacs complained first it cannot load 'haskell-ghci', hence I
downloaded 'haskell-ghci.el' and saved it in the same place when
haskell-mode is saved.
Then the error above.

Some ideas to fix it?