[Agda] Agda and Emacs mode

[Mateusz Kowalczyk]

On 12/10/2014 12:21 PM, Harley Eades III wrote:
> 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?

I did not have time to do any work regarding this. My list of ‘stuff I
need to hack on regarding Agda’ seems to always just grow and never
shrink. Unfortunately now even more than before I do not have time to
invest here. Maybe from February onwards… If someone wants to come up
with something then I would love to use it! Parsing what's effectively
ELisp and trying to re-implement the agda-mode.el functions to fit it is
rather ugly ;).

For reference, the response I was initially referring to is at
https://lists.chalmers.se/pipermail/agda/2014/007111.html

I wish luck to whoever decides to attempt to craft such API and
hopefully in the future I will have time to help out or do it myself if
not attempted yet.

> 
> Very best,
> .\ Harley
> 


-- 
Mateusz K.