# Generating LaTeX¶

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

$agda --latex {file}.lagda$ cd latex
$cd latex/$ perl ../postprocess-latex.pl {file}.tex > {file}.processed
$mv {file}.processed {file}.tex$ xelatex {file}.tex

Here is a full example, consisting of a Literate Agda file Example.lagda and a makefile Makefile.

Example.lagda
\documentclass{article}
\usepackage[references]{agda}

\begin{document}

Here we postulate \AgdaRef{apa}.

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

\end{document}
Makefile
AGDA=agda
AFLAGS=-i. --latex
SOURCE=Example
POSTPROCESS=postprocess-latex.pl
LATEX=latexmk -pdf -use-make -xelatex

all:
$(AGDA)$(AFLAGS) $(SOURCE).lagda cd latex/ && \ perl ../$(POSTPROCESS) $(SOURCE).tex >$(SOURCE).processed && \
mv $(SOURCE).processed$(SOURCE).tex && \
$(LATEX)$(SOURCE).tex && \
$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. 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). ### Including Agda code into a larger LaTeX document¶ Sometimes you might want to include a bit of code without necessarily making the whole document a literate Agda file. Here is how to do this in the context of a beamer presentation, but the method should work similarly also for other documents. Given two files Presentation.tex and Code.lagda as follows: Presentation.tex \documentclass{beamer} % When using XeLaTeX, the following should be used instead: % \documentclass[xetex]{beamer} % \usefonttheme[onlymath]{serif} \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} 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 -xelatex -pdf -use-make Presentation.tex

The \ExecuteMetaData command is part of the catchfilebetweentags package. Also see the following thread on the mailing list for other methods of including Agda code into a presentation.

## Options¶

The following command-line options change the behaviour of the LaTeX backend:

--latex-dir=directory
Changes the output directory where agda.sty and the output .tex are placed to directory. Default: latex.
--only-scope-checking
Generates highlighting without typechecking the file. See Quicker generation without typechecking.
--count-clusters
Count extended grapheme clusters when generating LaTeX code. This option can be given in OPTIONS pragmas. See Counting Extended Grapheme Clusters.

The following options can be given when loading agda.sty by using usepackage[options]agda:

bw
Colour scheme which highlights in black and white.
conor
Colour scheme similar to the colours used in Epigram1.
nofontsetup
Instructs the package to not select any fonts, and to not change the font encoding.
noinputencodingsetup
Instructs the package to not change the input encoding, and to not load the ucs package.
references
Enables inline typesetting of referenced code.

## Counting Extended Grapheme Clusters¶

The alignment feature regards the string , containing + and a combining character, as having length two. However, it seems more reasonable to treat it as having length one, as it occupies a single column, if displayed “properly” using a monospace font. The flag --count-clusters is an attempt at fixing this. When this flag is enabled the backend counts “extended grapheme clusters” rather than code points.

Note that this fix is not perfect: a single extended grapheme cluster might be displayed in different ways by different programs, and might, in some cases, occupy more than one column. Here are some examples of extended grapheme clusters, all of which are treated as a single character by the alignment algorithm:

│ │
│+̲│
│Ö̂│
│நி│
│ᄀힰᇹ│
│ᄀᄀᄀᄀᄀᄀힰᇹᇹᇹᇹᇹᇹ│
│ │

Note also that the layout machinery does not count extended grapheme clusters, but code points. The following code is syntactically correct, but if --count-clusters is used, then the LaTeX backend does not align the two field keywords:

record: Set₁ where  field A : Set
field B : Set

The --count-clusters flag is not enabled in all builds of Agda, because the implementation depends on the ICU library, the installation of which could cause extra trouble for some users. The presence of this flag is controlled by the Cabal flag enable-cluster-counting.

## Quicker generation without typechecking¶

A faster variant of the backend is available by invoking QuickLaTeX from the Emacs mode, or using agda --latex --only-scope-checking. When this variant of the backend is used the top-level module is not type-checked, only scope-checked. Note that this can affect the generated document. For instance, scope-checking does not resolve overloaded constructors.

If the module has already been type-checked successfully, then this information is reused; in this case QuickLaTeX behaves like the regular LaTeX backend.

## Known issues¶

The unicode-math package and older versions of the polytable package (still in the Debian stable) are incompatible, which can result in errors in generated latex code. The workaround is to download a more up to date version of polytable and either put it with the generated files, or install it globally.

## Complete LaTeX Template for Literate Agda with Unicode¶

This template has been tested under Debian and Ubuntu with TexLive, but should also work in other distributions. For xelatex or lualatex, only \usepackage{agda} should be needed.

\documentclass{article}

\usepackage{agda}

% 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).

\begin{document}

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

\end{document}