------------------------------------------------------------------------ To install Agda 2, proceed as follows: (An appendix below lists partial installation scripts for Ubuntu Linux.) 0) Install prerequisites (recent versions of GHC, Alex and Happy, and perhaps also darcs). GHC: http://www.haskell.org/ghc/ Alex: http://www.haskell.org/alex/ Happy: http://www.haskell.org/happy/ darcs: http://darcs.net/ In addition to the libraries distributed with GHC you will need the binary and zlib packages which can be downloaded from Hackage: http://hackage.haskell.org/cgi-bin/hackage-scripts/package/binary-0.4.1 http://hackage.haskell.org/cgi-bin/hackage-scripts/package/zlib-0.4.0.1 For non-Windows users: The zlib Haskell package requires the development files of the zlib C package to be installed (see http://zlib.net). Your package manager may be able to install these files for you. (For instance, on Debian or Ubuntu it should suffice to run apt-get install zlib1g-dev as root to get the correct files installed.) You will also need QuickCheck version 2, which can be obtained using darcs darcs get --partial http://darcs.haskell.org/QuickCheck or downloaded from http://www.cs.chalmers.se/~ulfn/files/QuickCheck-2.0.tar.gz 1) Download Agda 2, perhaps as follows: darcs get --partial http://code.haskell.org/Agda cd Agda 2) Build and install the Agda 2 library. If you want to install it in the default location (you may need root privileges for this), use the following commands: runhaskell Setup.hs configure runhaskell Setup.hs build runhaskell Setup.hs install You can select another location for the installation of the library by using the following commands: runhaskell Setup.hs configure --user --prefix= runhaskell Setup.hs build runhaskell Setup.hs install You can also give other options to the installation script, see runhaskell Setup.hs configure --help. 3) If you want to use the Emacs mode, build and install it (see below). 4) If you want to use the batch-mode Agda tool, go to the src/main directory, and build and install it: runhaskell Setup.hs clean # To ensure recompilation when upgrading. runhaskell Setup.hs configure runhaskell Setup.hs build runhaskell Setup.hs install Or: runhaskell Setup.hs clean runhaskell Setup.hs configure --user --prefix= runhaskell Setup.hs build runhaskell Setup.hs install When upgrading Agda, note that the batch-mode tool also needs to be rebuilt. ------------------------------------------------------------------------ To use the Agda 2 Emacs mode: -1. Install Emacs. (For non-Windows - jump down to **END OF "Under Windows ...") **Under Windows you may want to follow the following procedure: 1. Install NTEmacs 22. Download from http://ntemacs.sourceforge.net/ the self-extracting executable ntemacs22-bin-20070819.exe When executed, it asks where to extract itself. This can be anywhere you like, but here we write the top directory for ntemacs as c:/pkg/ntemacs in the following. What follows is tested only on this version. Other versions may work but you have to figure out yourself how to use Unicode fonts on your version. 2. Install ucs-fonts and mule-fonts for emacs. Download from http://www.cl.cam.ac.uk/~mgk25/ucs-fonts.html the tar file http://www.cl.cam.ac.uk/~mgk25/download/ucs-fonts.tar.gz Let us write the top directory of extracted files as c:/pkg/ucs-fonts Next we create some derived fonts. cd c:/pkg/ucs-fonts/submission make all-bdfs This gives an error message about missing fonts, but ignore it. Download from http://www.meadowy.org/ the tar file http://www.meadowy.org/meadow/dists/3.00/packages/mule-fonts-1.0-4-pkg.tar.bz2 The untarred top directory is named "packages", but we are only interested in the subdirectory "packages/fonts". Let us assume we moved this subdirectory to c:/pkg/mule-fonts Add the following to your .emacs ;;;;;;;;; start of quoted elisp code (setq bdf-directory-list '( "c:/pkg/ucs-fonts/submission" "c:/pkg/mule-fonts/intlfonts" "c:/pkg/mule-fonts/efonts" "c:/pkg/mule-fonts/bitmap" "c:/pkg/mule-fonts/CDAC" "c:/pkg/mule-fonts/AkrutiFreeFonts" )) (setq w32-bdf-filename-alist (w32-find-bdf-fonts bdf-directory-list)) (create-fontset-from-fontset-spec "-*-fixed-Medium-r-Normal-*-15-*-*-*-c-*-fontset-bdf, ascii:-Misc-Fixed-Medium-R-Normal--15-140-75-75-C-90-ISO8859-1, latin-iso8859-2:-*-Fixed-*-r-*-*-15-*-*-*-c-*-iso8859-2, latin-iso8859-3:-*-Fixed-*-r-*-*-15-*-*-*-c-*-iso8859-3, latin-iso8859-4:-*-Fixed-*-r-*-*-15-*-*-*-c-*-iso8859-4, cyrillic-iso8859-5:-*-Fixed-*-r-*-*-15-*-*-*-c-*-iso8859-5, greek-iso8859-7:-*-Fixed-*-r-*-*-15-*-*-*-c-*-iso8859-7, latin-iso8859-9:-*-Fixed-*-r-*-*-15-*-*-*-c-*-iso8859-9, mule-unicode-0100-24ff:-Misc-Fixed-Medium-R-Normal--15-140-75-75-C-90-ISO10646-1, mule-unicode-2500-33ff:-Misc-Fixed-Medium-R-Normal--15-140-75-75-C-90-ISO10646-1, mule-unicode-e000-ffff:-Misc-Fixed-Medium-R-Normal--15-140-75-75-C-90-ISO10646-1, japanese-jisx0208:-JIS-Fixed-Medium-R-Normal--16-150-75-75-C-160-JISX0208.1983-0, japanese-jisx0208-1978:-Misc-Fixed-Medium-R-Normal--16-150-75-75-C-160-JISC6226.1978-0, japanese-jisx0212:-Misc-Fixed-Medium-R-Normal--16-150-75-75-C-160-JISX0212.1990-0, latin-jisx0201:-*-*-medium-r-normal-*-16-*-*-*-c-*-jisx0201*-*, katakana-jisx0201:-Sony-Fixed-Medium-R-Normal--16-120-100-100-C-80-JISX0201.1976-0, thai-tis620:-Misc-Fixed-Medium-R-Normal--24-240-72-72-C-120-TIS620.2529-1, lao:-Misc-Fixed-Medium-R-Normal--24-240-72-72-C-120-MuleLao-1, tibetan:-TibMdXA-fixed-medium-r-normal--16-160-72-72-m-160-MuleTibetan-0, tibetan-1-column:-TibMdXA-fixed-medium-r-normal--16-160-72-72-m-80-MuleTibetan-1, korean-ksc5601:-Daewoo-Mincho-Medium-R-Normal--16-120-100-100-C-160-KSC5601.1987-0, chinese-gb2312:-ISAS-Fangsong ti-Medium-R-Normal--16-160-72-72-c-160-GB2312.1980-0, chinese-cns11643-1:-HKU-Fixed-Medium-R-Normal--16-160-72-72-C-160-CNS11643.1992.1-0, chinese-big5-1:-ETen-Fixed-Medium-R-Normal--16-150-75-75-C-160-Big5.ETen-0, chinese-big5-2:-ETen-Fixed-Medium-R-Normal--16-150-75-75-C-160-Big5.ETen-0 " t) (setq font-encoding-alist (append '( ("JISX0208" (japanese-jisx0208 . 0)) ("JISX0212" (japanese-jisx0212 . 0)) ("CNS11643.1992.1-0" (chinese-cns11643-1 . 0)) ("GB2312" (chinese-gb2312 . 0)) ("KSC5601" (korean-ksc5601 . 0)) ("VISCII" (vietnamese-viscii-lower . 0)) ("MuleArabic-0" (arabic-digit . 0)) ("MuleArabic-1" (arabic-1-column . 0)) ("MuleArabic-2" (arabic-2-column . 0)) ("muleindian-1" (indian-1-column . 0)) ("muleindian-2" (indian-2-column . 0)) ("MuleTibetan-0" (tibetan . 0)) ("MuleTibetan-1" (tibetan-1-column . 0)) ) font-encoding-alist)) ;;;;;;; end of quoted elisp code To test the fonts, try M-x eval-expression RET (set-default-font "fontset-bdf") RET M-x view-hello-file You should see all the characters without white-boxes. **END OF "Under Windows ..." 0. Install haskell-mode, version 2.1 or later (see http://haskell.org/haskell-mode/). Add (add-to-list 'load-path "") to your .emacs file. 1. Install Agda 2. (See above.) 2. Copy the .el files in src/full/Agda/Interaction/emacs-mode to some directory . Example installation: mkdir cp src/full/Agda/Interaction/emacs-mode/*.el 3. Add the following to your .emacs: (add-to-list 'load-path "") (require 'agda2) If you have already set up the suffix .agda for use with some other mode you may need to remove or alter that setting. You are encouraged to use the suffix .alfa for Agda 1 files. Now, if you open a file named XXX.agda the buffer will use agda2-mode. It may take 5 or 10 seconds before you see anything in the buffer, but that is normal. 4. If you want to you can customise some settings. Just start Emacs and type the following: M-x load-library RET agda2-mode RET M-x customize-group RET agda2 RET This is useful if you want to change the Agda search path, in which case you should change the agda2-include-dirs variable. 5. If you want some specific settings for the Emacs mode you can add them to agda2-mode-hook. For instance, if you do not want to use the Agda input method (for writing various symbols like ∀≥ℕ→π⟦⟧) you can add the following to your .emacs: (add-hook 'agda2-mode-hook '(lambda () ; If you do not want to use any input method: (inactivate-input-method) ; If you want to use the X input method: (set-input-method "X") )) A side note: In order to display Unicode characters you need to use a font which contains the glyphs in question. If such a font is not enabled by default (empty boxes are displayed instead of proper characters) you need to select another font. Do this by running M-x customize-face RET agda2-fontset-spec RET in Emacs (after you have started the Agda mode) and change the setting to a suitable font. ------------------------------------------------------------------ Appendix: Partial installation scripts for (at least) Ubuntu Linux (tested 080806 on Ubuntu 8.04 LTS) # A.0 Installing Haskell compilation tools sudo apt-get install ghc6 happy alex darcs # A.1 Installing binary wget http://hackage.haskell.org/packages/archive/binary/0.4.2/binary-0.4.2.tar.gz tar -zxf binary-0.4.2.tar.gz cd binary-0.4.2 runhaskell Setup.lhs configure runhaskell Setup.lhs build sudo runhaskell Setup.lhs install cd .. # A.2 Installing zlib sudo apt-get install zlib1g-dev wget http://hackage.haskell.org/packages/archive/zlib/0.4.0.4/zlib-0.4.0.4.tar.gz tar -zxf zlib-0.4.0.4.tar.gz cd zlib-0.4.0.4 runhaskell Setup.hs configure runhaskell Setup.hs build sudo runhaskell Setup.hs install cd .. # A.3 Installing mtl # If ubuntu is fresh enough: # sudo apt-get install libghc6-mtl-dev # otherwise wget http://hackage.haskell.org/packages/archive/mtl/1.1.0.1/mtl-1.1.0.1.tar.gz tar -zxf mtl-1.1.0.1.tar.gz cd mtl-1.1.0.1 runhaskell Setup.hs configure runhaskell Setup.hs build sudo runhaskell Setup.hs install cd .. # A.4 Installing QuickCheck 2 darcs get --partial http://darcs.haskell.org/QuickCheck cd QuickCheck runhaskell Setup.lhs configure runhaskell Setup.lhs build sudo runhaskell Setup.lhs install cd .. # A.5 Installing haskell-src sudo apt-get install libghc6-haskell-src-dev # Alt. get it from hackage: # wget http://hackage.haskell.org/packages/archive/haskell-src/1.0.1.2/haskell-src-1.0.1.2.tar.gz # ... # A.6 Installing Agda (including the stand-alone executable) # This has to be done from the root directory of an Agda distribution, # see point 1 above. runhaskell Setup.hs configure runhaskell Setup.hs build sudo runhaskell Setup.hs install cd src/main runhaskell Setup.hs configure runhaskell Setup.hs build sudo runhaskell Setup.hs install cd ../.. # A.7 [Optional] Download the Agda standard library sudo apt-get install autoconf autoconf ./configure make std-lib # A.8 [Optional] test the build make test