[Agda] Agda without emacs?

[Wolfram Kahl]

On Sat, Aug 13, 2011 at 04:17:02PM +0400, Grigory Sarnitskiy wrote:
> Hello! It is said that agda's interpreter is deprecated and emacs mode should be used instead.

It is still possible to use Agda without emacs
(or to use emacs only for editing, which is what I am doing most of the time).

The main disadvantage of typechecking from the terminal is that each new
Agda invocation has to reload all the (transitively) imported theories.
However, for me, the time for that is frequently negligible
compared with the typechecking time.

The main advantage of typechecking from the terminal is that
typechecking does not block editing.
(A second advantage is that you see more of what Agda is doing.)

The emacs mode also offers automated help
(the ``Auto'' command of the emacs mode is implemented by ``Agsy''),
which can be quite useful.

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

There is something on the Wiki about Agsy.
Useful hints may also be ``hidden'' in ALL release notes of stable Agda versions.


> Or alternatives to emacs.

(Somebody should connect Yi with Agda... --- nice project... ---  ;-)


Wolfram