README-2-2-8

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

  Table of contents:

  * Installing Agda
  * Configuring the Emacs mode
  * Prerequisites
  * Installing a suitable version of Emacs under Windows

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

    Note that this README only discusses installation of Agda, not its
    standard library. See the Agda Wiki for information about the
    library.

  There are several ways to install Agda:

  * Using a binary package, prepared for your platform.

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

  * Using a released source package, available from Hackage.

    (Note that if you want to install the development version of Agda,
    then you should use the next method.)

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

      cabal update
      cabal install Agda-executable
      agda-mode setup

    The last 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) Run the following commands in the top-level directory of the
        Agda source tree:

          cabal update
          cabal install
          agda-mode setup
          cd src/main
          cabal install

        The third 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.

    2b) Instead of following 2a you can try to install Agda (including
        batch-mode tool and Emacs mode) by running the following
        command:

          make install

  ------------------------------------------------------------------------
  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
  libraries zlib and ncurses are installed (see http://zlib.net and
  http://www.gnu.org/software/ncurses/). 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 libncurses5-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.
Page last modified on September 27, 2010, at 10:10 pm
Powered by PmWiki