[Agda] Agda without emacs?

[Christoph Herrmann]

Hi Grigory,

On 13 Aug 2011, at 13:17, Grigory Sarnitskiy wrote:

> Hello! It is said that agda's interpreter is deprecated and emacs mode should be used instead. However I have no experience with emacs (at least positive).

you don't need much in-depth knowledge of emacs, just normal computer science
installation knowledge, read the installation instructions, and some time to
install missing libraries explicitly. You can be lucky depending on your version of
ghc, cabal etc., but be prepared that it may take some time, e.g. for copying files
like haskell-ghci.el in the right directory and adding "provide ..." definitions
in the lisp files (you see how that works with looking at the other lisp files)

Warning: don't try to use XEmacs and similar variants. Although they
are generally most comfortable, they do not work with Agda. In particular 
they don't support the Unicode symbols, but there might be also other reasons;
I did not want to spend much time on trying to make the necessary adaptations.
Use gnu emacs or on MacOSX the Aquamacs emacs.

> Is there a tutorial or guide for using agda+emacs intended for noobs?

For using agda+emacs there is 
http://wiki.portal.chalmers.se/agda/pmwiki.php?n=Main.Documentation
The agda mode of emacs also has a drop-down menu.
However, I understood how these options are to be used effectively only
after having joined a training course. Nevertheless you should be able
to obtain the basic functionality by playing around with examples;
and maybe someone else can provide you with more information.

Important: "load" does a typecheck, for that you do not need to compile. 
Sometimes your emacs might seem to be blocked and this is not necessarily a 
bug but may be caused by a hard working type checker. Check the process list 
for the amount of CPU time the ghc process consumes. 

Good luck!
--
 Dr. Christoph Herrmann
 University of St Andrews, Scotland/UK
 phone: office: +44 1334 461629, home: +44 1334 478648 
 email: cah20 at st-andrews.ac.uk
 URL:   http://www.cs.st-andrews.ac.uk/~ch
 
 The University of St Andrews is a charity registered in Scotland: No SC013532