[Agda] Agda and Emacs mode

[Harley Eades III]

Hi, everyone.

On Dec 9, 2014, at 7:43 PM, Mateusz Kowalczyk <fuuzetsu at fuuzetsu.co.uk> wrote:

> On 12/10/2014 12:37 AM, Mateusz Kowalczyk wrote:
>> On 12/09/2014 11:27 AM, Andrej Bauer wrote:
>>> I have a master's student who would like to write a GUI for Agda on
>>> OSX (well, was told to do so).
>>> 
>>> I suggested that he should just hook into Agda's communication with
>>> Emacs. Is there reasonable documentation on how Agda communicates with
>>> Emacs?
>>> 
>>> Also, he now tells me that the Agda executable presupposes the
>>> existence of Emacs, which I have a hard time believing.
>>> 
>>> Can someone shed some light on how realistic a project this is?
>>> 
>>> With kind regards,
>>> 
>>> Andrej
>>> _______________________________________________
>>> Agda mailing list
>>> Agda at lists.chalmers.se
>>> https://lists.chalmers.se/mailman/listinfo/agda
>>> 
>> 
>> Some investigation was done
>> 
> 
> Apologies, didn't mean to send that, damn Thunderbird.
> 
> What I was going to say is that there was some investigation done into
> these commands by previous project (for the Atom editor I believe) but I
> can't find the file now. I started to do ‘the emacs way’ of talking to
> the process in Yi but it's very quickly becoming cumbersome. If your
> student is going to use Haskell, I recommend he does what Andreas
> recommended to me some weeks ago: collect the functions we want Agda to
> expose and try to establish an API proper, maintaining it between Agda
> releases.

I personally like the idea of an API instead of communicating with the emacs
interface.  This would make building various tools that need to use Agda in the
background much easier, and faster.  

One such tool I have been pondering about is a tool that allows one to do proofs
using graphical languages, e.g. string diagrams and proof nets. I would like
to write this in Haskell, but then generate the corresponding equational reasoning 
in Agda in the background. An API would make this a lot easier. 

Mateusz have you been working on an API?

Very best,
.\ Harley