[Agda] interaction interface
Peter Divianszky
divipp at gmail.com
Tue Apr 24 03:08:25 CEST 2012
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
More information about the Agda
mailing list