[Agda] Re: lhs2TeX for agda

[Darin Morrison]

Hi,

I had a similar problem recently.

The issue seems to be that lhs2TeX doesn't work properly with GHC 6.12 with the new I/O handling.  If you go back to 6.10 and recompile lhs2TeX then these errors go away and unicode parsing works fine.

What I did to work around this was to temporarily remove GHC 6.12, recompile lhs2TeX, then reinstall 6.12 and copy the appropriate files back over.  Kind of annoying but at least it works.

Hopefully it can be fixed in a future version.

Cheers,
Darin

On 16 Jul 2010, at 17:13, Neil Sculthorpe wrote:

> Hi Ondrej
> 
> I've had that error too.  I think it's objecting to unicode symbols.
> 
> I'm not sure if lhs2tex is supposed to be able to handle unicode, but replacing them with ASCII should help.  (And then writing a %format directive to turn them back into unicode).
> 
> Neil
> 
> On 16/07/10 16:38, Ondrej Rypacek wrote:
>> Hi Neil
>> 
>> Thanks, that makes a difference, indeed. Now I'm getting (the last few lines):
>> 
>> ...
>>   
>>> \begin{document}
>>> 
>>> We start with the module header:
>>> lhs2TeX: Enum.toEnum{Word8}: tag (8801) is outside of bounds (0,255)
>>>     
>> 
>> Cheers,
>> Ondrej
>> 
>> 
>> 
>> On 16 July 2010 12:48, Neil Sculthorpe<nas at cs.nott.ac.uk>  wrote:
>>   
>>> Hi Ondrej
>>> 
>>> I got the same error after installing lhs2tex 1.15 (though I'm on Ubuntu).
>>> 
>>> The problem seemed to be that the files in "/usr/local/share/lhs2tex-1.15/"
>>> (which includes Agda.fmt) were only readable by the user.  Setting them to
>>> be readable by all solved it for me.
>>> 
>>> Neil
>>> 
>>>     
> 
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda