Skip to content

Latest commit

 

History

History
281 lines (196 loc) · 11.1 KB

README.md

File metadata and controls

281 lines (196 loc) · 11.1 KB

Agda 2

Table of contents:

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:

Install using a binary package, prepared for your platform.

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

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

It is also possible (but not necessary) to compile the Emacs mode's files:

agda-mode compile

This can, in some cases, give a noticeable speedup.

WARNING: If you reinstall the Agda mode without recompiling the Emacs Lisp files, then Emacs may continue using the old, compiled files.

Install 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

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

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.

It is also possible (but not necessary) to compile the Emacs mode's files:

agda-mode compile

This can, in some cases, give a noticeable speedup.

WARNING: If you reinstall the Agda mode without recompiling the Emacs Lisp files, then Emacs may continue using the old, compiled files.

  1. Instead of following 2a you can try to install Agda (including a compiled 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:
            (deactivate-input-method)
            ; (In some versions of Emacs you should use
            ; inactivate-input-method instead of
            ; deactivate-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:

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 the Epic backend's dependencies

The Epic backend is experimental and requires that the Epic program is installed. You can install this program by giving the epic flag to cabal (but note that, at the time of writing, the Epic program does not build with certain recent versions of GHC):

When installing from Hackage:

cabal update
cabal install Agda -fepic
agda-mode setup

When installing using a source tar ball, following the instructions in 2a) above:

cabal update
cabal install -fepic
agda-mode setup

When installing using a source tar ball, following the instructions in 2b) above:

make CABAL_OPTIONS=-fepic install

You can also install Epic directly:

cabal install epic

Note that Epic depends on other software:

For more information about Epic: http://www.cs.st-andrews.ac.uk/~eb/epic.php

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. (Note: These instructions are possibly outdated.)

Step 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.

Step 2: Install ucs-fonts and mule-fonts for emacs.

Download from http://www.cl.cam.ac.uk/~mgk25/ucs-fonts.html the tar file at 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 at 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.