Installation of Agda from Source for Non-Programmers (Old Version 0)

These are the unofficial installation instructions, based on a version by Anton Setzer written for students with little experience in Linux and Haskell. They are written mainly with Linux in mind, but might be easily adapted for other operating systems. For the formal installation instructions refer to the official installation instructions for Agda.

• In order to get the latest sources of Agda, it is best to get darcs (brief instructions for darcs).
• Under Linux carry out the following as root, e.g. by ssh -X root@localhost
• Create a directory agda2 e.g. in /usr/local/src and move to this directory
• For getting the latest sources do

   darcs init
   darcs get --partial http://code.haskell.org/Agda

• That will create a directory Agda containing a file README with the official instructions for installing Agda.
• Install ghc 6.8.2 (brief instructions for ghc). Check version used with Offical download page for Agda.
• Install alex version 2.0 (brief instructions for alex), happy 1.15 (brief instructions for happy). Check version used with Offical download page for Agda.
• Install binary 0.4.1 (brief instructions for binary). Check version used with Offical download page for Agda.
• Install zlib 0.4.0.4 (brief instructions for zlib). Check version used with Offical download page for Agda.
• Install Quickcheck 2.1.0.1 (brief instructions for quickcheck). Check version used with Offical download page for Agda.
• Then go to the directory Agda created and do the cabal installation (How_to_install_a_Cabal_package).
  • There might be a problem with -lncurses. Download ncurses and ncurses-devel from my Linux distribution. Then the cabal installation should work.
• Then go to the subdirecory Agda/src/main and do again the Cabal installation. But first execute, in order to ensur recompilation when upgrading

   runghc Setup.hs clean

• This finishes the part to be done as root. Switch back to ordinary user (using exit).
• Then install the Emacs mode (Following Emacs conventions C-y stands in the following for Control-C and M-y for Alt-y or Escape-y):
  • Create a directory for the current agdainstallation ~/emacs/agdaByDate/2008/agdaDec2008/ (replace Dec2008 by the current month in the following)
  • Get the latest version of haskell mode from http://haskell.org/haskell-mode/
  • Move it to ~/emacs/agdaByDate/2008/agdaDec2008/ and untared it (using tar xvfz haskell-mode.tar.gz)
  • Copy the .el files in Agda/src/full/Agda/Interaction/emacs-mode/ to ~/emacs/agdaByDate/2008/agdaDec2008/
  • Create a file ~/emacs/agdainstall.el with content (~/emacs/agdainstall.el refers to the path where you put the .el files and the Haskell mode above).

<source lang="lisp">

   (setq load-path (cons "~/emacs/agdaByDate/2008/agdaDec2008/" load-path))
   (load "~/emacs/agdaByDate/2008/agdaDec2008/haskell-mode-2.4/haskell-site-file")
   (require 'agda2)

</source>

• (There are some possibilities for customisation of the emacs mode in the Agda2/README file )
• Comment out everything in .emacs regarding agda (putting ;; in front of it) in order to clean up my installation.
• Then add the following line to your .emacs file

  (load "~/emacs/agdainstall")

• Then start emacs and go to the files

  ~/.emacs

and all files in

  ~/emacs/agdaByDate/2008/agdaDec2008/*.el
  ~/emacs/agdaByDate/2008/agdaDec2008/*.el
  ~/emacs/agdaByDate/2008/agdaDec2008/haskell-mode-2.4/*.el

and do for each of them M-x byte-compile-file

• Then restart emacs, and open a file with extension .agda.

This file should start in agda mode.

• Note that Agda automatically adds certain abbreviations. In order to switch them off, execute M-x customize-group and then agda2 and then change the option Agda2 Mode Abbrevs Use Defaults: to No.

Installing the Standard Library

1. Follow the instructions under the same heading in the installation instructions for Mac OS.
2. Or do the following
   1. Download the Standard Library to any location you like through darcs:
      • darcs get --partial http://www.cs.nott.ac.uk/~nad/repos/lib/
   2. In Agda mode, enter the mode customization panel (M-x customize-mode).
   3. Look for the option Agda2 Include Dirs. Insert the path where you store the Standard Library.
   4. Click Save for Future Sessions.