[Agda] Writing a paper in Literate Agda

[Abhishek Anand]

Thanks Mateusz,
That helped a lot and I made some progress towards my modest
goal of putting some Agda code in a beamer presentation.

I used agda --latex and it made a directory latex/ containing the .tex file.

(I spend a lot of time trying to look for the .tex output in current
directory. Before that, I spent
some time trying to figure out why agda --latex was saying that the flag
--latex
is unrecognized. It turned out that --latex is not available in my older
version (2.3.0))

The .tex file compiles correctly and produces beautiful output.
Then, I copied relevant code to my beamer slide and got the following error:
--------------
! Package biblatex Error: Incompatible package 'ucs'.See the biblatex
package documentation for explanation.Type H <return> for immediate
help.... \begin{document}
-----------
It appears that agda.sty needs the ucs package.
I need biblatex to show citations as footnotes. I could't find any
alternative to biblatex.
I am not sure how to fix this issue.
It would be great if emacs could export to latex whatever it is rendering.
I couldn't find any way to do that. I tried using htmlfontify-buffer, but
it replaced all special characters with "?".

Any ideas about fixing this problem would be greatly appreciated.

Thanks,


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


On Thu, Nov 28, 2013 at 8:37 PM, Mateusz Kowalczyk
<fuuzetsu at fuuzetsu.co.uk>wrote:

> On 29/11/13 00:19, Abhishek Anand wrote:
> > Sorry for asking a beginner question.(Can't seem to find it on google).
> >
> > How does one generate a .lagda file from a .agda file
> > When I compile in windows, I get a .exe file
> > I also see some .agdai files
> >
>
> You don't generate .lagda files, you write your code in them. So for
> example, instead of writing in MyModule.agda, you would write in
> MyModule.lagda and then compile that. The difference is that you can use
> the literate syntax when using the .lagda file extension and the
> compiler should know what to do when it sees .lagda.
>
>
> --
> Mateusz K.
> _______________________________________________
> 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/20131201/fc15f9ec/attachment-0001.html