[Agda] Re: TeX capacity exceeded

[Abhishek Anand]

Is the problem fixed in the version 2.3.3 available via cabal?
(I'm getting errors while building Agda from sources.)
Also, is there a standard library that compatible with 2.3.3?
I'm getting the error:

abhishek at abhishek-VirtualBox:~/share/doc$ agda --latex -i
/home/abhishek/lib-0.7/src -i .  ext_univ.lagda
Checking ext_univ (/home/abhishek/share/doc/ext_univ.lagda).
 Checking Data.Product (/home/abhishek/lib-0.7/src/Data/Product.agda).
  Checking Function (/home/abhishek/lib-0.7/src/Function.agda).
   Checking Level (/home/abhishek/lib-0.7/src/Level.agda).
/home/abhishek/lib-0.7/src/Level.agda:27,1-32
Duplicate binding for built-in thing LEVEL, previous binding to
.Agda.Primitive.Level
when checking the pragma BUILTIN LEVEL Level



Thanks,

-- Abhishek
http://www.cs.cornell.edu/~aa755/


On Fri, Jan 10, 2014 at 10:39 AM, Stevan Andjelkovic <
stevan.andjelkovic at strath.ac.uk> wrote:

> Amr Sabry <sabry at ...> writes:
> >
> > [...]
> > When both definitions are included I get the error.
>
> Hi,
>
> The LaTeX-backend is still experimental, so I'd recommended pulling and
> building a fresh copy of Agda from the darcs repo when you run into
> problems
> with it.
>
> The problem was, as Andres pointed out, that the polytable part (used for
> alignment) of the LaTeX output was incorrect, this was fixed a month ago:
>
>   https://code.google.com/p/agda/issues/detail?id=990
>
>
> Cheers,
> SA.
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20140111/17921fff/attachment.html