[Agda] interaction interface

Peter Divianszky divipp at gmail.com
Tue Apr 24 03:08:25 CEST 2012


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.


More information about the Agda mailing list