Windows Installer Notes

Known Issues for the installer

  • Please check NotesOnInstaller.txt
  • Those who used the pre- 20110609 installer will have trouble with Emacs customization (once you customize anything, your .emacs will get broken). To remedy this, edit your .emacs and remove the two lines starting with '(agda2-ghci-options ...' and '(agda2-include-dirs ...' (in the arguments of `custom-set-variables'), or, simply remove your .emacs. Then use a post- 20110610 installer to re-install (prior uninstallation is not necessary).

How to completely remove Agda and Haskell

To get a clean slate for re-installation after a failed installation, you need to remove both Haskell and Agda. (The version numbers should be replaced as appropriate.)

  • Un-install Agda-2.2.10 and Haskell Platform 2011.2.0.1 from the Control Panel
  • Erase the folders:
    • For Windows 7 64-bit,
     C:\Program Files (x86)\Haskell
     C:\Program Files (x86)\Haskell Platform\2011.2.0.1
     C:\Program Files (x86)\Agda,
   plus maybe 
     C:\Users\$USER$\AppData\Local\VirtualStore\Program Files (x86)\Haskell
     C:\Users\$USER$\AppData\Local\VirtualStore\Program Files (x86)\Haskell Platform\2011.2.0.1
     C:\Users\$USER$\AppData\Local\VirtualStore\Program Files (x86)\Agda,
  • For Windows XP 32-bit,
     C:\Program Files\Haskell
     C:\Program Files\Haskell Platform\2011.2.0.1
     C:\Program Files\Agda,
     C:\Documents and Settings\$USER$\Application Data\cabal
     C:\Documents and Settings\$USER$\Application Data\ghc
  • Remove any mention of emacs and haskell from the system path.
  • Remove or rename your .emacs if you have any.

Shareware fonts

  • If you see meaningless boxes where you expect meaningful symbols, it is probably because the fontset your computer is using is not large enough; install and use the following fontset to recover this problem: Link to Code2000, a shareware covering wide range of unicode, or DejaVu font family with free licence.
  • Agda uses unicode, so allows you to use many mathematical/logical symbols. Not every font set, however, covers those mathematical/logical symbols, but the Code2000 fontset and DejaVu font family both cover a reasonable subset.

Older Versions 2012-11-05 links no longer works due to a host relocation; if they did, various external dependencies have made them disfunctional...

Upgrading darcs: OBSOLETE: Upgrading function has been removed from the installer.

Some old versions of the installer did not support darcs 2. You can fix this by reinstalling Agda using a new installer, or by following the instructions below.

  1. Download a new version of darcs and extract it to agda2\bin.
  2. Delete agda2\Agda, agda2\lib

Excute the following commands:

  1. darcs get --lazy
  2. darcs get --lazy

Done. You could run Agda2\Update to update.

OBSOLETE: Interim instruction for Agda-2.2.10 installation

(Version numbers referred is slightly outdated. The newer ones should work ... until they break things.)

  1. Download and install Haskell Platform for Windows from
  2. Download and install GNU unifont from
    • Download the zip file
    • Unzip the zip file
    • Open the Font folder by: Start -> Control Panel -> (Classic view) -> Font
    • At the Font folder: File -> Install New Font, then choose the unziped file.
  3. Download and install Emacs-23 (This is an example suitable for Japanese IME users; other Emacs-23 on Windows would probably work) This is a part of gnupack (in Japanese)
    • Execute emacs-23.2-20110219.exe and extract the contents to somewhere.
      For example, choosing "C:\MyPrograms" creates a new folder "C:\MyPrograms\eamcs-23.2-20110219" (Avoid CJK characters in a path.)
    • Modify the Path environment variable to include "C:\MyPrograms\emacs-23.2-20110219\bin"
  4. Download and install Haskell-mode for emacs