[Agda] interaction interface

[Ramana Kumar]

I just want to say thank you for making this excellent start on improving
the interface :)

On Tue, Apr 24, 2012 at 2:08 AM, Peter Divianszky <divipp at gmail.com> wrote:

> Hi,
>
> Recently I have made steps to improve the Agda interaction interface.
> These changes are not visible for the end users, but as a side effect the
> Agda source and binary distributions have less dependencies.
>
> The changes are already in the darcs repository:
>
> * A new Response data type describes the possible interaction responses.
> You can find it in the module Agda.Interaction.Response. Previously the
> response was a String.
>
> * The Agda Emacs mode now calls the agda executable instead of ghci. As an
> effect the Agda binary distributions does not depend on GHC and the Haskell
> libraries. Also the memory consumption and startup time should be better (I
> didn't measured these).
>
> * The Agda Emacs mode does not depend on haskell-mode any more. This was
> easy to achieve because the dependency was very weak.
>
> Thanks for Nils for ensuring to make these changes correctly and also for
> fixing bugs which was caused by the changes.
>
> The next steps could be the following:
>
> * Make a Request data type similar to Response.
> * Make the *ghci* buffer optional and hidden by default - the end users
> should not be interested in it.
> * Don't require comint in agda2-mode.el - call agda directly via pipes.
>
> The last two changes would improve the interaction speed slightly and
> later we could develop more interactions without trouble.
>
> After these changes there are a lots of possibilities too.
> We could arrive to a common interactive frontend for dependently typed
> languages, somewhat like the common idris backend.
> This frontend could liberate Agda from Emacs too.
>
> Unfortunately I will not have time for these changes so I present these
> plans for discussion.
>
> Cheers,
> Peter
>
>
>
> ______________________________**_________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/**mailman/listinfo/agda<https://lists.chalmers.se/mailman/listinfo/agda>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20120424/9a65e588/attachment.html