[Agda] emacs problems

[Nils Anders Danielsson]

On 2009-06-16 23:01, Andreas Buechele wrote:

> ---8<---
> Prelude Agda.Interaction.GhciTop> cmd_goal_type_context
> Agda.Interaction.BasicOps.Normalised 0 (Range [Interval (Pn
> "SomeAgdaFile.agda" 2260 52 41) (Pn "SomeAgdaFile.agda" 2260 52 41)]) ""
> 
> <interactive>:1:254: lexical error at character '\EOT'
> Prelude Agda.Interaction.GhciTop>
> --->8---

The problem is that, when GHC 6.10 is used on certain platforms, there
is an upper limit to the length of strings that can be sent to GHCi from
Emacs shell buffers:

  http://code.google.com/p/agda/issues/detail?id=136

The limit seems to be higher for 6.10.1 and 6.10.2, so I would currently
advise against using Agda with GHC 6.10.3 under Linux. I have not
encountered these problems when using GHC 6.8.3.

I have reported this problem to the developers of both GHC and
haskeline, but they claim that the problem lies with Emacs, and it seems
as if the Emacs developers consider this to be a feature rather than a
bug.

One way out of this situation is to stop using GHCi to communicate with
the Agda backend. I think it would be good if there was a well-defined
interface between the frontend and the backend, because then it would be
easier to construct new frontends. However, I don't have time to
construct such an interface now. It would be great if someone else could
do it; such an interface can be developed with relatively little
knowledge of the Agda internals, and plenty of help would be available
from the current Agda developers.

-- 
/NAD

This message has been checked for viruses but the contents of an attachment
may still contain software viruses, which could damage your computer system:
you are advised to perform your own checks. Email communications with the
University of Nottingham may be monitored as permitted by UK legislation.