<div dir="ltr">Is the problem fixed in the version 2.3.3 available via cabal?<div>(I'm getting errors while building Agda from sources.)</div><div>Also, is there a standard library that compatible with 2.3.3?</div><div>
I'm getting the error:</div><div><pre style="word-wrap:break-word"><font color="#000000"><span style="white-space:pre-wrap">abhishek@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</span></font><span style="color:rgb(0,0,0);white-space:pre-wrap">
</span></pre></div><div><br></div><div><br></div><div>Thanks,</div></div><div class="gmail_extra"><br clear="all"><div><div>-- Abhishek</div><a href="http://www.cs.cornell.edu/~aa755/" target="_blank">http://www.cs.cornell.edu/~aa755/</a></div>
<br><br><div class="gmail_quote">On Fri, Jan 10, 2014 at 10:39 AM, Stevan Andjelkovic <span dir="ltr"><<a href="mailto:stevan.andjelkovic@strath.ac.uk" target="_blank">stevan.andjelkovic@strath.ac.uk</a>></span> wrote:<br>
<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">Amr Sabry <sabry@...> writes:<br>
><br>
> [...]<br>
<div class="im">> When both definitions are included I get the error.<br>
<br>
</div>Hi,<br>
<br>
The LaTeX-backend is still experimental, so I'd recommended pulling and<br>
building a fresh copy of Agda from the darcs repo when you run into problems<br>
with it.<br>
<br>
The problem was, as Andres pointed out, that the polytable part (used for<br>
alignment) of the LaTeX output was incorrect, this was fixed a month ago:<br>
<br>
<a href="https://code.google.com/p/agda/issues/detail?id=990" target="_blank">https://code.google.com/p/agda/issues/detail?id=990</a><br>
<br>
<br>
Cheers,<br>
SA.<br>
<div class="HOEnZb"><div class="h5"><br>
_______________________________________________<br>
Agda mailing list<br>
<a href="mailto:Agda@lists.chalmers.se">Agda@lists.chalmers.se</a><br>
<a href="https://lists.chalmers.se/mailman/listinfo/agda" target="_blank">https://lists.chalmers.se/mailman/listinfo/agda</a><br>
</div></div></blockquote></div><br></div>