========================================================================
Agda 2
========================================================================
Table of contents:
* Installing Agda
* Configuring the Emacs mode
* Prerequisites
* Installing the Epic backend's dependencies
* 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
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.
* 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.
2b) 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:
(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/
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.
--------