README-2–2−6

 ========================================================================
 Agda 2
 ========================================================================

 Table of contents:

 * Installing Agda
 * Configuring the Emacs mode
 * Prerequisites
 * Installing a suitable version of Emacs under Windows
 * Installation script for (at least) Ubuntu

 ------------------------------------------------------------------------
 Installing Agda
 ------------------------------------------------------------------------

 There are several ways to install Agda. (Note that this README only
 discusses installation of Agda, not its standard library. See the Agda
 Wiki for information about the library.)

 * Using a binary package, prepared for your platform.

   Recommended if such a package exists. See the Agda Wiki.

 * Using stable packages available from Hackage.

   Install the prerequisites mentioned below, then run the following
   commands:

     cabal install Agda-executable
     agda-mode setup

   The second command tries to set up Emacs for use with Agda. As an
   alternative you can copy the following text to your .emacs file:

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

 * Using the source tar balls available from the Agda Wiki, or the
   development version of the code available from our darcs repository.

   1)  Install the prerequisites mentioned below.

   2a) If your system is Unix-like you can now hopefully install the
       Agda 2 library, batch-mode tool and Emacs mode by running the
       following command:

         make install

       If this does not work on your system, or you want to have more
       control, you can follow 2b instead.

   2b) Run the following commands in the top-level directory of the
       Agda source tree:

         cabal install
         agda-mode setup
         cd src/main
         cabal clean       # To ensure recompilation when upgrading.
         cabal install

       The second command tries to set up Emacs for use with Agda. As
       an alternative you can copy the following text to your .emacs
       file:

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

       If you want to have more control over where files are installed
       then you can give various flags to cabal install, see
       cabal install --help.

   A section below lists an installation script which should work under
   the Ubuntu distribution of GNU/Linux, assuming that your
   configuration is reasonably standard.

 ------------------------------------------------------------------------
 Configuring the Emacs mode
 ------------------------------------------------------------------------

 If you want to you can customise the Emacs mode. 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.

 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")
              ))

 Note that, on some systems, the Emacs mode changes the default font of
 the current frame in order to enable many Unicode symbols to be
 displayed. This only works if the right fonts are available, though.
 If you want to turn off this feature, then you should customise the
 agda2-fontset-name variable.

 ------------------------------------------------------------------------
 Prerequisites
 ------------------------------------------------------------------------

 You need recent versions of the following programs/libraries:

    GHC:           http://www.haskell.org/ghc/
    cabal-install: http://www.haskell.org/cabal/
    Alex:          http://www.haskell.org/alex/
    Happy:         http://www.haskell.org/happy/
    GNU Emacs:     http://www.gnu.org/software/emacs/
    haskell-mode:  http://projects.haskell.org/haskellmode-emacs/

 You should also make sure that programs installed by cabal-install are
 on your shell's search path.

 For instructions on installing a suitable version of Emacs under
 Windows, see below.

 Non-Windows users need to ensure that the development files for the C
 library zlib are 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.

 ------------------------------------------------------------------------
 Installing a suitable version of Emacs under Windows
 ------------------------------------------------------------------------

 Note that Agda code often uses mathematical and other symbols
 available from the Unicode character set. In order to be able to
 display these characters you may want to follow the procedure below
 when installing Emacs under Windows.

 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.

 ------------------------------------------------------------------------
 Installation scripts for Ubuntu 9.10
 ------------------------------------------------------------------------

 Installs a released version:

   sudo apt-get install agda-mode agda-bin

 Installs the development version:

   sudo apt-get install ghc6 happy alex darcs emacs haskell-mode zlib1g-dev make
   wget http://www.haskell.org/cabal/release/cabal-install-0.6.4/cabal-install-0.6.4.tar.gz
   tar xzf cabal-install-0.6.4.tar.gz
   cd cabal-install-0.6.4
   . bootstrap.sh
   cd ..
   $HOME/.cabal/bin/cabal update
   darcs get --lazy http://code.haskell.org/Agda
   cd Agda
   make CABAL_CMD="$HOME/.cabal/bin/cabal" install