Latest installation of Agda2 with all other programs needed
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Files containing additional information for packages and 
 other programs:
  darcsinstallPublicParts.txt
  ghcinstallPublicParts.txt
  alexinstallPublicParts.txt 
  happyinstallPublicParts.txt  
  cabalPublicParts.txt)
See as well 
http://wiki.portal.chalmers.se/agda/
(Note that, as far as I know, Version 2.1.2 doesn't
 contain yet the termination and coverage checker,
 which is crucial for the module interactive theorem proving)

For downloading the latest versions of Agda and Quickcheck,
I needed darcs see file darcsinstallPublicParts.txt
(I recommend to get the latest sources using darcs,
to have all bug fixes - however you can get the
versions I used for building Agda successfully from my
agdainstallation page)

I created a directory agda2

In there I did 
  darcs init
  darcs get --partial http://code.haskell.org/Agda
for getting agda2
(See my website for the last version I used for building Agda2)

That directory contains a file README which gives
the official and very detailed description  of how to 
install Agda.


I installed ghc 6.8.2 binary package Linux (x86) 
  using the version using libreadline.so.5 isntead of libreadline.so.4 (in case of
    32 bit, for 64 bit there seems to be no difference any more between the two versions)
  See file ghcinstallPublicParts.txt
  (On one machine I needed to install gmp-32bit (message showed problem with libgmp.so.4, which I got from my linux distribution Suse 10.1)
Note that ghc can be installed locally.

Then I installed alex and happy (see files alexinstallPublicParts.txt and happyinstallPublicParts.txt which refers to 
 file  cabalPublicParts.txt)

Then I installed the binary package 

 http://hackage.haskell.org/cgi-bin/hackage-scripts/package/binary-0.4.1

(binary 0.4.2 doesn't work for Agda, it want's exactly binary 0.4.1)
 
  (which was installed using the standard cabal installation machinery )


I had problems building it.
  But then I realised I had to install the glibc package from Suse
  and glibc-devel


Then I installed the zlib package 
 I used 0.4.0.2 (not 0.4.0.1 as recommended)
 (latest built: I aused 0.4.0.4)

 http://hackage.haskell.org/cgi-bin/hackage-scripts/package/zlib-0.4.0.2

I had problems building it first.
Then I downloaded from my Linux distribution the
zlib-devel package
(I downloaded some more packages concerning zlib, but I think the zlib-devel,
 as mentioned in the agda README file was the one needed)
Then I deleted the directory of zlib with its contents, created it again
Then the cabal installation machinery worked (see file cabalPublicParts.txt)


Then I needed Quickcheck 2.0
which I got
by using

darcs get http://www.cs.chalmers.se/~bringert/darcs/QuickCheck/

(See my website for the latest version which worked for me)

This created a directory QuickCheck
from there I did the cabal installation (see file cabalPublicParts.txt)

Then I went to the agda directory
and did there the cabal installation (see file cabalPublicParts.txt)

Then I went to src/main
and did the same
But there was a problem with -lncurses

I downloaded ncurses and ncurses-devel from my Linux distribution.
Then the cabal installation worked.

Then I installed the emacs mode:
I created a directory for my current agdainstallation
~/emacs/agdaByDate/2008/agdaJan2008/

I got the latest version of haskell mode
http://haskell.org/haskell-mode/

I moved it to ~/emacs/agdaByDate/2008/agdaJan2008/
  and untared it (using tar xvfz haskell-mode.tar.gz)

I copied the .el files in Agda/src/full/Agda/Interaction/emacs-mode/
~/emacs/agdaByDate/2008/agdaJan2008/


Then I created a file ~/emacs/agdainstall.el

with content (~/emacs/agdaByDate/2008/agdaJan2008/ refers
  to the path where I put the .el files and the haskell mode above)

(setq load-path (cons "~/emacs/agdaByDate/2008/agdaJan2008/" load-path))
(setq load-path (cons "~/emacs/agdaByDate/2008/agdaJan2008/haskell-mode-2.4/" load-path))
(autoload 'agda2-mode "agda2-mode" "Agda2 mode." t)
(add-to-list 'auto-mode-alist '("\\.l?agda$" . agda2-mode))
(modify-coding-system-alist 'file "\\.l?agda$" 'utf-8)
(add-hook 'agda2-mode-hook
             '(lambda nil
                (require 'quail)
                (set-input-method 'TeX)
                ))


(There are some possibilities for customisation 
of the emacs mode in the Agda2/README file )

I commented out everything in .emacs regarding agda (putting ;; in front of it)


Then I added the following line to my .emacs file

(load "~/emacs/agdainstall")





Then I started emacs and went to the files

~/.emacs
all files in
~/emacs/agdaByDate/2008/agdaJan2008/*.el
~/emacs/agdaByDate/2008/agdaJan2008/*.el
~/emacs/agdaByDate/2008/agdaJan2008/haskell-mode-2.4/*.el

and did there

M-x byte-compile-file

Then I restarted emacs, and opening a file with extension .agda
agda mode should be started.