[Agda] Agda on GitHub Atom

[Helmut Grohne]

On Sat, Apr 12, 2014 at 11:56:48PM +0530, Balaji Rao R wrote:
> I’m interested to develop an Agda package for the GitHub Atom editor. Can anyone give me pointers on how to get started on the Agda side ? I would like to start by trying to get highlighting to work.

The basic issue is that the better syntax highlighting relies on type
checking. I am aware of 4 ways to highlight Agda:

 * Use agda --html or agda --latex (uses type checking).
 * Emacs agda2-mode (uses type checking by running agda in a separate
   process).
 * Vim can use agda --vim output files for highlighting see
   http://wiki.portal.chalmers.se/agda/pmwiki.php?n=Main.VIMEditing
   (uses type checking), but one can also use the generic syntax file
   without type checking to achieve very limited highlighting
 * lhs2TeX has very very limited highlighting (no type checking used for
   highlighting).

In any case there is more to editing Agda than just highlighting.
Working with "holes" and "goals" is essential. "Just" highlighting helps
with reading Agda code, but is little help for writing.

http://oxij.org/note/BrutalDepTypes/ is one of the introductions that
describes the process of editing in addition to describing the language.
As far as I can tell the Emacs editing experience is currently unmatched
by any other tool in the Agda world. 

Helmut