[Agda] Agda error reporting

kahl at cas.mcmaster.ca kahl at cas.mcmaster.ca
Sat Apr 10 23:04:28 CEST 2010


On Sat, 10 Apr 2010, Ulf Norell wrote:
 > 
 > On Fri, Apr 9, 2010 at 11:23 PM, <kahl at cas.mcmaster.ca> wrote:
 > 
 > >
 > > The latest development version of Agda (my first pull since quite a while)
 > > seems to truncate error messages to the first three lines when called
 > > from the command line.
 > > (Being on PowerPC, I don't have ghci, so I normally use the command line.)
 > >
 > 
 > That's a unicode issue. We switched to using the unicode support that comes
 > with the ghc libraries, and there's a problem that if your terminal isn't
 > configured for unicode it just truncates the output.

Thank you for the clarification! (I also had started to suspect that since.)

 > I can't remember the exact details but making
 > sure your terminal can display unicode will make the problem go away.

Does anybody know a terminal+settings combination that works?
``display unicode'' seems to be simply said...

I tried to tune rxvt-unicode, without success,
and I just tried gnome-terminal, and don't see more there, either,
although it came up with STIXSize1 as font, looking somewhat funny...



By the way, something you did recently reduced memory usage significantly
(the only changes entry I saw that looked relevant
 was that about removing traces), so right now I have some theories going
through in (far less than) 3G heap
that before didn't go through in 4GB address space --- thanks a lot!


I fought a bit with GHC-6.12.1.20100330 yesterday,
and I won ;-) , by removing Terminfo from Haskeline,
so now i have GHCi again
(not every time, but it usually starts after a few attempts).
What is the best way to limit the heap for Agda running inside emacs?
Could one also pass in +RTS -S and actually see the result in the ghci
buffer? My emacs seems to be completely irresponsive while Agda is running.
(Which is one reason why I tend to run Agda in a terminal.)


Wolfram


More information about the Agda mailing list