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
   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.