<div class="gmail_extra">I just want to say thank you for making this excellent start on improving the interface :)<br><br><div class="gmail_quote">On Tue, Apr 24, 2012 at 2:08 AM, Peter Divianszky <span dir="ltr"><<a href="mailto:divipp@gmail.com" target="_blank">divipp@gmail.com</a>></span> wrote:<br>
<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">Hi,<br>
<br>
Recently I have made steps to improve the Agda interaction interface.<br>
These changes are not visible for the end users, but as a side effect the Agda source and binary distributions have less dependencies.<br>
<br>
The changes are already in the darcs repository:<br>
<br>
* 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.<br>
<br>
* 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).<br>
<br>
* The Agda Emacs mode does not depend on haskell-mode any more. This was easy to achieve because the dependency was very weak.<br>
<br>
Thanks for Nils for ensuring to make these changes correctly and also for fixing bugs which was caused by the changes.<br>
<br>
The next steps could be the following:<br>
<br>
* Make a Request data type similar to Response.<br>
* Make the *ghci* buffer optional and hidden by default - the end users should not be interested in it.<br>
* Don't require comint in agda2-mode.el - call agda directly via pipes.<br>
<br>
The last two changes would improve the interaction speed slightly and later we could develop more interactions without trouble.<br>
<br>
After these changes there are a lots of possibilities too.<br>
We could arrive to a common interactive frontend for dependently typed languages, somewhat like the common idris backend.<br>
This frontend could liberate Agda from Emacs too.<br>
<br>
Unfortunately I will not have time for these changes so I present these plans for discussion.<br>
<br>
Cheers,<br>
Peter<br>
<br>
<br>
<br>
______________________________<u></u>_________________<br>
Agda mailing list<br>
<a href="mailto:Agda@lists.chalmers.se" target="_blank">Agda@lists.chalmers.se</a><br>
<a href="https://lists.chalmers.se/mailman/listinfo/agda" target="_blank">https://lists.chalmers.se/<u></u>mailman/listinfo/agda</a><br>
</blockquote></div><br></div>