Agda2 Installation

The following contains the information about how Anton Setzer succeeded to install Agda under Linux and Windows. This is a very rough version, which is not yet well formatted and worked out. Please watch out at this place for improved versions.

Web pages.
- Agda (Wikipedia)
- Agda home page (covers mainly Agda1 at present)
- The Agda Wiki (contains some documentation, downloads; note that Version 2.1.2 doesn't have the coverage and termination checker, which is required for the coursework in the module Interactive Theorem Proving).
All instructions for installations in the following are without any warranty. See each package/program for its license.
Instructions on installing Agda2 in the Linux Lab (CS department, Swansea University)
Installation of Agda under Linux
- agdainstallPublicParts.txt (main instructions).
- Additional packages and programs used:
  - darcsinstallPublicParts.txt (darcs)
  - cabalPublicParts.txt (Use of Cabal)
  - ghcinstallPublicParts.txt (ghc)
  - alexinstallPublicParts.txt (alex)
  - happyinstallPublicParts.txt (happy)
  - The file contains additional material, which facilitates the use of Agda.
Installation of Agda under Windows
- agdawindowsinstallPublicParts.txt (main instructions).
- Additional packages and programs used:
  - darcsinstallPublicParts.txt (darcs)
  - cabalPublicParts.txt (Use of Cabal)
  - perlwindowsinstallPublicParts.txt (Perl)
  - alexwindowsinstallPublicParts.txt (alex)
  - happywindowsinstallPublicParts.txt (happy)
  - binaryhaskellwindowsinstallPublicParts.txt (binary)
  - zlibhaskellwindowsinstallPublicParts.txt (zlib)
  - The file contains additional material, which facilitates the use of Agda.
Additional Material (list of symbols for the leim mode under Agda, use and activation of abbreviation mode.
Downloading of some packages
- It is recommended to use darcs following the above instructions in order to obtain the latest version, which contains some bug fixes.
- If you don't know how to install darcs, or have problems installing is, here are the latest version downloaded by Anton Setzer, from which he was able to build Agda2 successfully.
  - QuickCheck.zip
  - Agda2.zip
Help with Unicode input
- List of leim symbols under Agda
- Use of the abbreviation mode, which makes typing in special symbols much easier

Anton Setzer

Last modified: Wed Jan 14 14:15:10 GMT 2009