Generating LaTeX

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

  1. $ agda --latex {file}.lagda
  2. $ cd latex
  3. $ {latex-compiler} {file}.tex

where _latex-compiler_ could be pdflatex, xelatex or lualatex, and _file_.lagda is a literate Agda TeX file (it could also be called _file_.lagda.tex). The source file is expected to import the LaTeX package agda by including the code \usepackage{agda} (possibly with some options). Unlike the HTML backend only the top-most module is processed. Imported modules can be processed by invoking agda --latex manually on each of them.

The LaTeX backend checks if agda.sty is found by the LaTeX environment. If it isn’t, a default agda.sty is copied into the LaTeX output directory (by default latex). Note that the appearance of typeset code can be modified by overriding definitions from agda.sty.

Note

The agda.sty shipped with Agda is located at _${Agda_datadir_}/latex/agda. Since version 2.6.2, the Agda data directory can be printed using the option :option:–print-agda-dir`, which has been an alias of --print-agda-data-dir since 2.6.4.1. Thus, you can get hold of the class file via cat $(agda --print-agda-data-dir)/latex/agda.sty.

Known pitfalls and issues

  • Unicode characters may not be typeset properly out of the box. How to address this problem depends on what LaTeX engine is used.

    • pdfLaTeX:

      The pdfLaTeX program does not by default understand the UTF-8 character encoding. You can tell it to treat the input as UTF-8 by using the inputenc package:

      1. \usepackage[utf8]{inputenc}

      If the inputenc package complains that some Unicode character is “not set up for use with LaTeX”, then you can give your own definition. Here is one example:

      1. \usepackage{newunicodechar}
      2. \newunicodechar{λ}{\ensuremath{\mathnormal\lambda}}
      3. \newunicodechar{←}{\ensuremath{\mathnormal\from}}
      4. \newunicodechar{→}{\ensuremath{\mathnormal\to}}
      5. \newunicodechar{∀}{\ensuremath{\mathnormal\forall}}

    • XeLaTeX or LuaLaTeX:

      It can sometimes be easier to use LuaLaTeX or XeLaTeX. When these engines are used it might suffice to choose a suitable font, as long as it contains all the right symbols in all the right shapes. If it does not, then \newunicodechar can be used as above. Here is one example:

      1. \usepackage{unicode-math}
      2. \setmathfont{XITS Math}
      4. \usepackage{newunicodechar}
      5. \newunicodechar{λ}{\ensuremath{\mathnormal\lambda}}

      In recent versions of LuaLaTeX, you can avoid using \newunicodechar at all by instead setting up a chain of fallback fonts, e.g.

      1. \usepackage{luaotfload}
      2. \directlua{luaotfload.add_fallback
      3.   ("mycustomfallback",
      4.     { "SymbolamonospacifiedforSourceCodePro:style=Regular;"
      5.     , "NotoSansMono:style=Regular;"
      6.     , "NotoSansMath:style=Regular;"
      7.     }
      8.   )}
      9. \defaultfontfeatures{RawFeature={fallback=mycustomfallback}}

  • If < and > are typeset like ¡ and ¿, then the problem might be that you are using pdfLaTeX and have not selected a suitable font encoding.

    Possible workaround:

    1. \usepackage[T1]{fontenc}

  • If a regular text font is used, then -- might be typeset as an en dash (–).

    Possible workarounds:

    • Use a monospace font.

    • Turn off ligatures. With pdfLaTeX the following code (which also selects a font encoding, and only turns off ligatures for character sequences starting with -) might work:

      1. \usepackage[T1]{fontenc}
      2. \usepackage{microtype}
      3. \DisableLigatures[-]{encoding=T1}

      With LuaLaTeX or XeLaTeX the following code (which also selects a font) might work:

      1. \usepackage{fontspec}
      2. \defaultfontfeatures[\rmfamily]{}
      3. \setmainfont{Latin Modern Roman}

      Note that you might not want to turn off all kinds of ligatures in the entire document. See the Examples below for information on how to set up special font families without TeX ligatures that are only used for Agda code.

  • The unicode-math package and older versions of the polytable package are incompatible, which can result in errors in generated LaTeX code.

    Possible workaround: Download a more up-to-date version of polytable and put it together with the generated files or install it globally.

Options

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

--latex-dir={DIR}

Changes the output directory where agda.sty and the output .tex file are placed to _DIR_. 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 Epigram 1.

references

Enables inline typesetting of referenced code.

links

Enables hyperlink support.

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.

Features

Vertical space

Code blocks are by default surrounded by vertical space. Use \AgdaNoSpaceAroundCode{} to avoid this vertical space, and \AgdaSpaceAroundCode{} to reenable it.

Note that, if \AgdaNoSpaceAroundCode{} is used, then empty lines before or after a code block will not necessarily lead to empty lines in the generated document. However, empty lines inside the code block do (by default, with or without \AgdaNoSpaceAroundCode{}) lead to empty lines in the output. The height of such empty lines can be controlled by the length \AgdaEmptySkip, which by default is \abovedisplayskip.

Alignment

Tokens preceded by two or more space characters, as in the following example, are aligned in the typeset output:

  1. \begin{code}
  2. data ℕ : Set where
  3.   zero  : ℕ
  4.   suc   : ℕ → ℕ
  6. _+_ : ℕ → ℕ → ℕ
  7. zero   + n = n
  8. suc m  + n = suc (m + n)
  9. \end{code}

In the case of the first token on a line a single space character sometimes suffices to get alignment. A constraint on the indentation of the first token t on a line is determined as follows:

  • Let T be the set containing every previous token (in any code block) that is either the initial token on its line or preceded by at least one whitespace character.

  • Let S be the set containing all tokens in T that are not shadowed by other tokens in T. A token t₁ is shadowed by t₂ if t₂ is further down than t₁ and does not start to the right of t₁.

  • Let L be the set containing all tokens in S that start to the left of t, and E be the set containing all tokens in S that start in the same column as t.

  • The constraint is that t must be indented further than every token in L, and aligned with every token in E.

Note that if any token in L or E belongs to a previous code block, then the constraint may not be satisfied unless (say) the AgdaAlign environment is used in an appropriate way. If custom settings are used, for instance if \AgdaIndent is redefined, then the constraint discussed above may not be satisfied.

Examples:

  • Here C is indented further than B:
  1. postulate
  2.    A  B
  3.        C : Set
  • Here C is not (necessarily) indented further than B, because X shadows B:
  1. postulate
  2.    A  B  : Set
  3.    X
  4.        C : Set

These rules are inspired by, but not identical to, the one used by lhs2TeX’s poly mode (see Section 8.4 of the manual for lhs2TeX version 1.17).

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:

  1. │ │
  2. │+̲│
  3. │Ö̂│
  4. │நி│
  5. │ᄀힰᇹ│
  6. │ᄀᄀᄀᄀᄀᄀힰᇹᇹᇹᇹᇹᇹ│
  7. │ │

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:

  1. record +̲ : Set₁ where  field A : Set
  2.                         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.

Breaking up code blocks

Sometimes one might want to break up a code block into multiple pieces, but keep code in different blocks aligned with respect to each other. Then one can use the AgdaAlign environment. Example usage:

  1.  \begin{AgdaAlign}
  2.  \begin{code}
  3.    code
  4.      code  (more code)
  5.  \end{code}
  6.  Explanation...
  7.  \begin{code}
  8.    aligned with "code"
  9.      code  (aligned with (more code))
  10. \end{code}
  11. \end{AgdaAlign}

Note that AgdaAlign environments should not be nested.

Sometimes one might also want to hide code in the middle of a code block. This can be accomplished in the following way:

  1. \begin{AgdaAlign}
  2. \begin{code}
  3.   visible
  4. \end{code}
  5. \begin{code}[hide]
  6.   hidden
  7. \end{code}
  8. \begin{code}
  9.   visible
  10. \end{code}
  11. \end{AgdaAlign}

However, the result may be ugly: extra space is perhaps inserted around the code blocks. The AgdaSuppressSpace environment ensures that extra space is only inserted before the first code block, and after the last one (but not if \AgdaNoSpaceAroundCode{} is used). Example usage:

  1. \begin{AgdaAlign}
  2. \begin{code}
  3.   code
  4.     more code
  5. \end{code}
  6. Explanation...
  7. \begin{AgdaSuppressSpace}
  8. \begin{code}
  9.   aligned with "code"
  10.     aligned with "more code"
  11. \end{code}
  12. \begin{code}[hide]
  13.   hidden code
  14. \end{code}
  15. \begin{code}
  16.     also aligned with "more code"
  17. \end{code}
  18. \end{AgdaSuppressSpace}
  19. \end{AgdaAlign}

Note that AgdaSuppressSpace environments should not be nested. There is also a combined environment, AgdaMultiCode, that combines the effects of AgdaAlign and AgdaSuppressSpace.

Hiding code

Code that you do not want to show up in the output can be hidden by giving the argument hide to the code block:

  1. \begin{code}[hide]
  2. -- the code here will not be part of the final document
  3. \end{code}

Hyperlinks (experimental)

If the hyperref latex package is loaded before the agda package and the links option is passed to the agda package, then the agda package provides a function called \AgdaTarget. Identifiers which have been declared targets, by the user, will become clickable hyperlinks in the rest of the document. Here is a small example:

  1. \documentclass{article}
  2. \usepackage{hyperref}
  3. \usepackage[links]{agda}
  4. \begin{document}
  6. \AgdaTarget{ℕ}
  7. \AgdaTarget{zero}
  8. \begin{code}
  9. data ℕ : Set where
  10.   zero  : ℕ
  11.   suc   : ℕ → ℕ
  12. \end{code}
  14. See next page for how to define \AgdaFunction{two} (doesn't turn into a
  15. link because the target hasn't been defined yet). We could do it
  16. manually though; \hyperlink{two}{\AgdaDatatype{two}}.
  18. \newpage
  20. \AgdaTarget{two}
  21. \hypertarget{two}{}
  22. \begin{code}
  23. two : ℕ
  24. two = suc (suc zero)
  25. \end{code}
  27. \AgdaInductiveConstructor{zero} is of type
  28. \AgdaDatatype{ℕ}. \AgdaInductiveConstructor{suc} has not been defined to
  29. be a target so it doesn't turn into a link.
  31. \newpage
  33. Now that the target for \AgdaFunction{two} has been defined the link
  34. works automatically.
  36. \begin{code}
  37. data Bool : Set where
  38.   true false : Bool
  39. \end{code}
  41. The AgdaTarget command takes a list as input, enabling several targets
  42. to be specified as follows:
  44. \AgdaTarget{if, then, else, if\_then\_else\_}
  45. \begin{code}
  46. if_then_else_ : {A : Set} → Bool → A → A → A
  47. if true then t else f = t
  48. if false then t else f = f
  49. \end{code}
  51. \newpage
  53. Mixfix identifier need their underscores escaped:
  54. \AgdaFunction{if\_then\_else\_}.
  56. \end{document}

The borders around the links can be suppressed using hyperref’s hidelinks option:

  1. \usepackage[hidelinks]{hyperref}

Warning

The current approach to links does not keep track of scoping or types, and hence overloaded names might create links which point to the wrong place. Therefore it is recommended to not overload names when using the links option at the moment. This might get fixed in the future.

Numbered code listings

When the option number is used an equation number is generated for the code listing. The number is set to the right, centered vertically. By default the number is set in parentheses, but this can be changed by redefining \AgdaFormatCodeNumber.

The option can optionally be given an argument: when number=l is used a label l, referring to the code listing, is generated. It is possible to use this option several times with different labels.

An example:

  1. \begin{code}[number=code:lemma]
  2.   a proof
  3. \end{code}
  4. %
  5. A consequence of Lemma~\ref{code:lemma} is that…

The option number has no effect if used together with hide, inline or inline*.

Inline code

Code can be typeset inline by giving the argument inline to the code block:

  1. Assume that we are given a type
  2. %
  3. \begin{code}[hide]
  4.   module _ (
  5. \end{code}
  6. \begin{code}[inline]
  7.     A : Set
  8. \end{code}
  9. \begin{code}[hide]
  10.     ) where
  11. \end{code}
  12. %
  13. .

There is also a variant of inline, inline*. If inline* is used, then space (\AgdaSpace{}) is added at the end of the code, and when inline is used space is not added.

The implementation of these options is a bit of a hack. Only use these options for typesetting a single line of code without multiple consecutive whitespace characters (except at the beginning of the line).

Another way to typeset inline code

An alternative to using inline and inline* is to typeset code manually. Here is an example:

  1. Below we postulate the existence of a type called
  2. \AgdaPostulate{apa}:
  3. %
  4. \begin{code}
  5.   postulate apa : Set
  6. \end{code}

You can find all the commands used by the backend (and which you can use manually) in the agda.sty file.

Semi-automatically typesetting inline code (experimental)

Since Agda version 2.4.2 there is experimental support for semi-automatically typesetting code inside text, using the references option. After loading the agda package with this option, inline Agda snippets will be typeset in the same way as code blocks—after post-processing—if referenced using the \AgdaRef command. Only the current module is used; should you need to reference identifiers in other modules, then you need to specify which other module manually by using \AgdaRef[module]{identifier}.

In order for the snippets to be typeset correctly, they need to be post-processed by the postprocess-latex.pl script from the Agda data directory. You can copy it into the current directory by issuing the command

  1. $ cp $(agda --print-agda-data-dir)/latex/postprocess-latex.pl .

In order to generate a PDF, you can then do the following:

  1. $ agda --latex {file}.lagda
  2. $ cd latex/
  3. $ perl ../postprocess-latex.pl {file}.tex > {file}.processed
  4. $ mv {file}.processed {file}.tex
  5. $ xelatex {file}.tex

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

Example.lagda

  1. \documentclass{article}
  2. \usepackage[references]{agda}
  4. \begin{document}
  6. Here we postulate \AgdaRef{apa}.
  7. %
  8. \begin{code}
  9.   postulate apa : Set
  10. \end{code}
  12. \end{document}

Makefile

  1. AGDA=agda
  2. AFLAGS=-i. --latex
  3. SOURCE=Example
  4. POSTPROCESS=postprocess-latex.pl
  5. LATEX=latexmk -pdf -use-make -xelatex
  7. all:
  8.     $(AGDA) $(AFLAGS) $(SOURCE).lagda
  9.     cd latex/ && \
  10.     perl ../$(POSTPROCESS) $(SOURCE).tex > $(SOURCE).processed && \
  11.     mv $(SOURCE).processed $(SOURCE).tex && \
  12.     $(LATEX) $(SOURCE).tex && \
  13.     mv $(SOURCE).pdf ..

See Issue #1054 on the bug tracker for implementation details.

Warning

Overloading identifiers should be avoided. If multiple identifiers with the same name exist, then AgdaRef will typeset according to the first one it finds.

Controlling the typesetting of individual tokens

The typesetting of (certain) individual tokens can be controlled by redefining the \AgdaFormat command. Example:

  1. \usepackage{ifthen}
  3. % Insert extra space before some tokens.
  4. \DeclareRobustCommand{\AgdaFormat}[2]{%
  5.   \ifthenelse{
  6.     \equal{#1}{≡⟨} \OR
  7.     \equal{#1}{≡⟨⟩} \OR
  8.     \equal{#1}{∎}
  9.   }{\ }{}#2}

Note the use of \DeclareRobustCommand. The first argument to \AgdaFormat is the token, and the second argument the thing to be typeset.

Emulating %format rules

The LaTeX backend has no feature directly comparable to lhs2TeX’s %format rules. However, one can hack up something similar by using a program like sed. For instance, let us say that replace.sed contains the following text:

  1. # Turn Σ[ x ∈ X ] into (x : X) ×.
  2. s/\\AgdaRecord{Σ\[} \(.*\) \\AgdaRecord{∈} \(.*\) \\AgdaRecord{]}/\\AgdaSymbol\{(\}\1 \\AgdaSymbol\{:\} \2\\AgdaSymbol\{)\} \\AgdaFunction\{×\}/g

The output of the LaTeX backend can then be postprocessed in the following way:

  1. $ sed -f replace.sed {file}.tex > {file}.sedded
  2. $ mv {file}.sedded {file}.tex

Including Agda code in a larger LaTeX document

Sometimes you might want to include a bit of code without making the whole document a literate Agda file. There are two ways in which this can be accomplished.

(The following technique was probably invented by Anton Setzer.) Put the code in a separate file, and use \newcommand to give a name to each piece of code that should be typeset:

Code.lagda.tex

  1. \newcommand{\nat}{%
  2. \begin{code}
  3. data ℕ : Set where
  4.   zero  : ℕ
  5.   suc   : (n : ℕ) → ℕ
  6. \end{code}}

Preprocess this file using Agda, and then include it in another file in the following way:

Main.tex

  1. % In the preamble:
  2. \usepackage{agda}
  3. % Further setup related to Agda code.
  5. % The Agda code can be included either in the preamble or in the
  6. % document's body.
  7. \input{Code}
  9. % Then one can refer to the Agda code in the body of the text:
  10. The natural numbers can be defined in the following way in Agda:
  11. \nat{}

Here it is assumed that agda.sty is available in the current directory (or on the TeX search path).

Note that this technique can also be used to present code in a different order, if the rules imposed by Agda are not compatible with the order that you would prefer.

There is another technique that uses the catchfilebetweentags latex package. Assuming you have some code in Code.lagda and want to include it in Paper.tex, you first add tags to your code as follows:

Code.lagda

  1. %<*nat>
  2. \begin{code}
  3. data ℕ : Set where
  4.   zero  : ℕ
  5.   suc   : (n : ℕ) → ℕ
  6. \end{code}
  7. %</nat>
  9. %<*plus>
  10. \begin{code}
  11. _+_ : ℕ → ℕ → ℕ
  12. zero   + n = n
  13. suc m  + n = suc (m + n)
  14. \end{code}
  15. %</plus>

You can then use \ExecuteMetaData, as provided by catchfilebetweentags, to include the code. Note that the code does not have to be in the same order (or from the same files). This method is particularly convenient when you want to write a paper or presentation about a library of code.

Paper.tex

  1. % Other setup related to Agda...
  2. \usepackage{catchfilebetweentags}
  4. \begin{document}
  6.   \begin{itemize}
  7.     \item The natural numbers
  8.   \end{itemize}
  10.   \ExecuteMetaData[latex/Code.tex]{nat}
  12.   \begin{itemize}
  13.     \item Addition (\AgdaFunction{\_+\_})
  14.   \end{itemize}
  16.   \ExecuteMetaData[latex/Code.tex]{plus}

Examples

Some examples that can be used for inspiration (in the HTML version of the manual you see links to the source code and in the PDF version of the manual you see inline source code).

Note that these examples might not satisfy all your requirements, and might not work in all settings (in particular, for LuaLaTeX or XeLaTeX it might be necessary to install one or more fonts). If you have to follow a particular house style, then you may want to make sure that the Agda code follows this style, and that you do not inadvertently change the style of other text when customising the style of the Agda code.