Literate Agda

Agda supports a limited form of literate programming out of the box. If you name your source files Something.lagda, then all the code has to appear in code blocks:

 \begin{code}
 module Whatever where

 ...
 \end{code}

The text outside the code blocks is ignored. If you provide a suitable definition for the code environment, then literate Agda files can double as LaTeX document sources. Example definition:

 \usepackage{verbatim}
 \newenvironment{code}{\verbatim}{\endverbatim}

The preprocessor lhs2TeX can also handle literate Agda files.

Unicode and LaTeX

LaTeX does not by default understand the UTF-8 character encoding. You can tell LaTeX to treat the input as UTF-8 by inserting the following code in the preamble of your source file:

 \usepackage{ucs}
 \usepackage[utf8x]{inputenc}

The ucs package does not contain definitions for all Unicode characters. If LaTeX complains about a missing definition for some character U+xxxx, then you can define it yourself:

 \DeclareUnicodeCharacter{"xxxx}{<definition>}

It may also be necessary to instruct LaTeX to use a specific font encoding. The autofe package tries to select the font encoding automatically:

 \usepackage{autofe}

(Note that the lhs2TeX support files for Agda already do something similar to the steps above.)

A complete LaTeX template for literate Agda with Unicode

This has been tested under ubuntu with texlive, but should work in other distributions:

 \documentclass{article}

 % The following packages are needed because unicode
 % is translated (using the next set of packages) to
 % latex commands. You may need more packages if you
 % use more unicode characters:

 \usepackage{amssymb}
 \usepackage{bbm}
 \usepackage[greek,english]{babel}

 % This handles the translation of unicode to latex:

 \usepackage{ucs}
 \usepackage[utf8x]{inputenc}
 \usepackage{autofe}

 % Some characters that are not automatically defined
 % (you figure out by the latex compilation errors you get),
 % and you need to define:

 \DeclareUnicodeCharacter{8988}{\ensuremath{\ulcorner}}
 \DeclareUnicodeCharacter{8989}{\ensuremath{\urcorner}}
 \DeclareUnicodeCharacter{8803}{\ensuremath{\overline{\equiv}}}

 % Add more as you need them (shouldn't happen often).

 % Using "\newenvironment" to redefine verbatim to
 % be called "code" doesn't always work properly. 
 % You can more reliably use:

 \usepackage{fancyvrb}

 \DefineVerbatimEnvironment
   {code}{Verbatim}
   {} % Add fancy options here if you like.

 \begin{document}

 \begin{code}
   ... your Agda code goes here ...
 \end{code}

 \end{document}

The LaTeX-backend

An experimental LaTeX-backend was added in Agda 2.3.2. It can be used as follows:

  agda --latex <file>.lagda
  cd latex
  <latex-compiler> <file>.tex

where <latex-compiler> could be pdflatex, xelatex or lualatex. See the release notes for versions 2.3.2 and 2.3.4 for further details and examples: http://code.haskell.org/Agda/CHANGELOG

Making up for the lack of lhs2TeX's %format rules

The LaTeX-backend has no feature analogue to lhs2TeX's %format rule, however most systems come with sed which can be used to achieve similar goals. Given a file called, for example, replace.sed containing:

    http://lpaste.net/raw/8093650300608446464

We can postprocess the tex output as follows:

    sed -f replace.sed <file>.tex > <file>.sedded 
    mv <file>.sedded <file>.tex 

Note that the above sed file assumes the use of {xe|lua}latex where code is in math mode rather than text mode (as is the case when using the pdflatex compiler). The commented out variants of the substitution rules are their pdflatex equivalents (see next section before using them though).

The substitution rules dealing with super- and subscripts lets us write apa^bepa in the code for things we want superscripted in the output (\undertie does the same for subscripts).

Manually typesetting inline code

The backend only typesets code inside code blocks, inline code you have to typeset manually, e.g.:

  Below we postulate a set called \AgdaDatatype{apa}.

  \begin{code}
  postulate apa : Set
  \end{code}

You can find all the commands used by the backend (and which you can use manually) in the latex/agda.sty file. If you are doing a lot of manual typesetting, then you might want to introduce shorter command names, e.g.:

  \newcommand{\D}{\AgdaDatatype}
  \newcommand{\F}{\AgdaFunction}

etc. Long names were chosen by default to avoid name clashes.

Semi-automatically typesetting inline code

Since Agda version 2.4.2 there is experimental support for semi-automatically typesetting code inside text, using the references option. Here is a full example.

Example.lagda

    
    \documentclass{article}
    \usepackage[references]{agda} 
    \begin{document}

    Here we postulate \AgdaRef{apa}.

    \begin{code}
    postulate apa : Set
    \end{code}

    \end{document}
    

Makefile

Note that postprocess-latex.pl can be found in the Agda data dir, i.e. issue cp $(dirname $(dirname $(agda-mode locate)))/postprocess-latex.pl . (once) before make.

    
    AGDA=agda
    AFLAGS=-i. --latex
    SOURCE=Example
    POSTPROCESS=postprocess-latex.pl
    LATEX=latexmk -pdf -use-make -e '$$pdflatex=q/xelatex %O %S/'

    all:
        $(AGDA) $(AFLAGS) $(SOURCE).lagda
        cd latex/ && \
        perl ../$(POSTPROCESS) $(SOURCE).tex > $(SOURCE).processed && \
        mv $(SOURCE).processed $(SOURCE).tex && \
        $(LATEX) $(SOURCE).tex && \
        mv $(SOURCE).pdf ..
    

Implementation details

See https://code.google.com/p/agda/issues/detail?id=1054 for implementation details.

{xe|lua}latex and proper unicode fonts

LaTeX was never written with unicode in mind, hacks like the ucs package makes it possible to use them, but for the best possible output consider using xelatex or lualatex instead.

The default math font in agda.sty is limited though (many characters are missing). The XITS font is more complete:

    http://www.ctan.org/tex-archive/fonts/xits/

Simply save the .otf files into ~/.fonts, use:

    \setmainfont{XITS}
    \setmathfont{XITS Math}

in agda.sty, and compile the output using:

    latexmk -pdf -e '$pdflatex=q/lualatex %O %S/' <file>.tex

Using Beamer together with the LaTeX-backend to create slides for talks

Sometimes you might want to include a bit of code without necessarily making the whole document a literate Agda file. The following section describes how to do this in the context of a beamer presentation, but should work similarly for a document. Given the two files Presentation.tex:

    \documentclass{beamer}

    % When using XeLaTeX, the following should be used instead:
    % \documentclass[xetex, mathserif, serif]{beamer}
    %
    % The default font in XeLaTeX doesn't have the default bullet character, so 
    % either change the font:
    % \setmainfont{XITS}
    % \setmathfont{XITS Math}
    %
    % Or change the character:
    %\setbeamertemplate{itemize items}{}

    \usepackage{latex/agda}
    \usepackage{catchfilebetweentags}

    \begin{document}
    \begin{frame}\frametitle{Some Agda code}

      \begin{itemize}
        \item The natural numbers
      \end{itemize}

      \ExecuteMetaData[latex/Code.tex]{nat}

      \begin{itemize}
        \item Addition (\AgdaFunction{\_+\_})
      \end{itemize}

      \ExecuteMetaData[latex/Code.tex]{plus}

    \end{frame}
    \end{document}

and Code.lagda:

    %<*nat>
    \begin{code}
    data ℕ : Set where
      zero  : ℕ
      suc   : (n : ℕ) → ℕ
    \end{code}
    %</nat>

    %<*plus>
    \begin{code}
    _+_ : ℕ → ℕ → ℕ
    zero   + n = n
    suc m  + n = suc (m + n)
    \end{code}
    %</plus>

we can use pdflatex to compile a presentation as follows:

  agda --latex Code.lagda
  latexmk -pdf -use-make Presentation.tex

If you are using a lot of unicode it might be more convenient to use xelatex instead. See comments about xelatex in Presentation.tex and compile as follows:

  agda --latex Code.lagda
  latexmk -e '$pdflatex=q/xelatex S/' -pdf -use-make Presentation.tex

With a sufficently new version of latexmk one can use the -xelatex-flag instead of the -e '...' stuff.

The \ExecuteMetaData command is part of the neat catchfilebetweentags package, which you can read more about here:

  http://mirrors.ctan.org/macros/latex/contrib/catchfilebetweentags/catchfilebetweentags.pdf

Also see the following thread on the mailing list for other methods of including Agda code into a presentation:

  http://comments.gmane.org/gmane.comp.lang.agda/6195

"Can we produce a document without doing typechecking every time?"

No, typechecking is essential to the typesetting (otherwise we don't know what colours etc to use).

However, since lhs2tex and the latex backend are interchangeable (or should be at least), I suppose you could have a "fast" and a "slow" make target, e.g. a Makefile with:

  
  COMPILER=latexmk -pdf -use-make -e '$$pdflatex=q/xelatex %O %S/'

  fast:
        lhs2tex --agda <file>.lagda > latex/<file>.tex
        cd latex && \
        $(COMPILER) <file>.tex && \
        mv <file>.pdf ..

  slow:
        agda --latex <file>.lagda
        cd latex && \
        $(COMPILER) <file>.tex && \
        mv <file>.pdf ..
  

Then you can compile using "make fast" to avoid typechecking (at the cost of not having colours etc).

Known issues

unicode-math and (oldish versions of) polytable are incompatible. See this bug report:

    https://github.com/kosmikus/lhs2tex/issues/29

Error messages generated by latex usually look like:

    ! Argument of ... has an extra }.