[Agda] Simplified installation of the Emacs mode

Nils Anders Danielsson nad at Cs.Nott.AC.UK
Wed Apr 8 12:18:13 CEST 2009


Hi,

The Agda packages on Hackage do not contain the Emacs mode. This is
annoying, so in the latest development version I have changed things so
that cabal install also installs the Emacs mode. The directory in which
the mode is installed depends on a number of factors, including the
version of Agda, so I wrote a program called agda-mode which prints out
the path to agda2.el. This program can be used in .emacs:

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

(I included functionality in agda-mode which asks Emacs for the location
of the user's .emacs file and inserts the code above, but this may be
mostly a novelty.)

The Emacs mode has also been changed: it now requests a fixed version of
the Agda library. Previously people have encountered problems when they
have upgraded the Agda library but not the Emacs mode, because sometimes
the interface between them has changed. This should not be a problem
anymore (except perhaps for people using the development version of
Agda; the developers should remember to change the version number when
the interface is changed).

I plan to release a new version of Agda, including these changes,
relatively soon. However, because the changes are slightly disruptive
(users will have to change their .emacs files when upgrading) I first
want to hear if there are any objections to them.

-- 
/NAD


This message has been checked for viruses but the contents of an attachment
may still contain software viruses, which could damage your computer system:
you are advised to perform your own checks. Email communications with the
University of Nottingham may be monitored as permitted by UK legislation.



More information about the Agda mailing list