Installation of Agda from Source for Non-Programmers

NOTE: THE FOLLOWING INSTRUCTIONS ARE SERIOUSLY OUTDATED! (Mine them for hints or stay away!)

Please update the following instructions, if you have any problems with this instructions and found a way to solve them.

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. An older version can be found here, which might give you some hints how to get around some problems with installing Agda.

• During the following installation, you might need some additional packages from your Linux or other operating system distribution.
  • The following have occurred at previous occasions:
  • If you get an error message checking for curses.h ... no then you need to install curses.h Installing ncurses and ncurses-devel from Suse worked, under Ubuntu I used libncurses5-dev.
  • If you need a GLU C library, install the package mesa-devel (for me mesa-devel-7.2.10.1 worked) from your distribution.
  • If you get the problem that curl.h headers are missing, install libcurl.devel or any other devel version of the curl library.
• The main installation is as follows:
• Work as root
• Install GHC 6.10.3 (you might try using later versions of GHC)
  • If your distribution has a package for GHC 6.10.3, install it using your package manager (this includes Fedora 11 and OpenSUSE 11.1, but not Debian 5.0 ("Lenny") or Ubuntu 9.04 ("Jaunty")). Otherwise:
  • Download it from http://www.haskell.org/ghc/
  • unpack it using

    tar xvjf <file>.tar.bz2

• Go to the created directory and follow the README file for installation instructions.
• Check using ghc --version which version of GHC you have.
• If this command fails or doesn't return 6.10.3 identify where ghc was installed (e.g. using the README file of ghc). Add the directory to your path (by adding in ~/.bashrc the line export PATH=<newpath>:$PATH with <newpath> being the path to your ghc file (e.g. /usr/local/bin/)

• Download a few Haskell packages from Hackage: http://hackage.haskell.org/packages/archive/pkg-list.html
• For each of them:
  • unpack them (tar xvzf <file>.tar.gz)
  • go to the subdirectory created and execute (Setup.hs might have to be replaced by Setup.lhs)

    runghc Setup.hs configure
    runghc Setup.hs build
    runghc Setup.hs install

• If during configure it says that another package is missing, download it as well from Hackage and do the procedure as above.

• The packages you need to get from Hackage in order to get the cabal install tool running are:
  • HTTP (4000.0.7)
  • cabal (1.6.0.2) (Note that this does not install the cabal command. Only when you install the cabal-install tool below you will get the cabal command).
  • zlib (0.4.0.4) (You might need zlib-devel and gmp-devel from your general software management system in order to be able to install it.)
• You might be able to get these from your package manager. But only do this if you also installed GHC this way, and make sure it gives you the right versions. Use 'ghc-pkg field <package> version' to check.
• Now download from http://haskell.org/cabal/download.html the cabal install tool (0.6.2). Do the same procedure as before (or with Setup.hs replaced by Setup.lhs)

   runghc Setup.hs configure
   runghc Setup.hs build
   runghc Setup.hs install

• Now you can use cabal for installing future packages.
• In order to be able to automatically download packages execute

   cabal update

• This updates the database from the Hackage repository. Now in future in order to install a package from Hackage you only need to run

    cabal install --global <package name>

(this will install the package for all users on your system) or, for a local installation,

    cabal install <package name>

• Now install Agda-exectuable:

   cabal install --global Agda-executable
   agda-mode setup

• if you have problems with terminfo, this might be because you need curses. See the entry on curses at the beginning of this description.
• if you have problems with not having the version of happy needed, try installing a newer version of ghc (7.0.3 worked)
• you might need to get from your distribution GLUT-devel and OpenGL-devel.

• The command agda-mode setup will install the .emacs mode into your .emacs file, but probably only for the user you are in. For every local user you can have to repeat the command

   agda-mode setup

or add the following lines to your .emacs file:

   (load-file (let ((coding-system-for-read 'utf-8))
   (shell-command-to-string "agda-mode locate")))

• Finally you need to install the Haskell mode for Emacs. If this mode cannot be installed using your package manager you may want to try the following instructions:
  • Get it from http://www.iro.umontreal.ca/~monnier/elisp/#haskell-mode
  • Unpack it and move it somewhere where emacs has read access (e.g. in a directory ~/emacs/haskell-mode/). Add to your .emacs file the following line:

    (setq load-path (cons "<path>" load-path))

   where <path> is replaced by the path to your Haskell mode (e.g. if you moved it to ~/emacs/haskell-mode then <path> is ~/emacs/haskell-mode)

• You might have to run M-x byte-compile-file on your .emacs file if you ever compiled it in order to get an up-to-date version.

• Now load an Agda file.
  • Examples can be found at http://www.cs.chalmers.se/~ulfn/darcs/Agda2/examples/Introduction/
  • A quick guide on how to use Agda can be found here: QuickGuideToEditingTypeCheckingAndCompilingAgdaCode
  • If there are any problems with loading the file (it takes too long), run from Emacs quit C-g, switch to the buffer *ghci* and check what's going on.
  • Possible problems:
    • you are not using the right version of ghci
    • you haven't installed the packages using the global option
    • you are using the wrong configuration file. Then delete an entry of the form: export GHC_PACKAGE_PATH=<your entry> from your file ~/.bashrc
• You might want to download the standard library from Libraries.StandardLibrary
• You might need to customize Agda (e.g. setting the load path)
  • When in an Agda buffer use from the menu of emacs Options -> Customize Emacs -> Top level customization group -> Programming -> Languages -> Agda2
  • Especially make sure that Agda2 Include Directories contains . and the path to any library you want (e.g. the standard library)
• More information is available from Main.HomePage