lagda.md2tex

Introduction

This repository provides a tool to convert literate Agda files written in markdown to LaTeX. A common source can be used to produce both .pdf and .html files. The source can include diagrams written in Tikz, and these will appear in both the produced .pdf and .html. The tool uses LuaTeX (available as part of TeXLive), which has good support for unicode.

Literate Agda may be written either in LaTeX (with extension .lagda.tex) or markdown (with extension .lagda.md). Including code blocks in LaTeX is easy while including inline code may be painful, requiring LaTeX macros for special characters or special unicode declarations. In contrast, in markdown both code blocks and inline code are easy.

The repository also provides a monospace font assembled from several open source fonts that provides a wide range of monospaced unicode characters, in particular, all those that are used in the textbook PLFA.

The subdirectory examples includes examples of how to typeset an academic paper for both JFP and PACMPL.

Install dependencies

The project depends on the following software:

• Agda: for type checking and highlighting literate Agda files.
• Pandoc: for converting files from markdown format to others.
• TeX Live: for LuaTeX, which has good Unicode support.
• pdf2svg: for generating images from LaTeX code. The linked document has instructions for Windows and Linux. On a Mac, use brew install pdf2svg to install the software.
• Python: a programming language needed by pandoc-latex-environment
• pandoc-latex-environment: for parsing div blocks in markdown to latex

Install the font

Under font there is a font file called DejaVu mononoki Symbola Droid. It is a custom combined monospace font that covers a wide range of Unicode symbols. Install the font globally on your system. On Mac, you need to first set Font Book - Preferences - Default Install Location to 'Computer' before installing.

Setup makefile

1. Clone this repo to your local machine
2. Copy makefile, main.tex, main.md, template.html, and style.css to your project.
3. Near the top of makefile, set three variables. i. SRC holds the path to the source file directory. ii. FILTERS holds the path to pandoc-filters in this repository. iii. MAIN holds the name of the output files. Its value is set to main by default. The tool produces <MAIN>.pdf (in the root directory) and (in the html subdirectory) <MAIN>.html .

Adjust the template files

Each file <FILE>.lagda.md in subdirectory src will be processed to generate files latex/<FILE>.tex and html/<FILE>.html. There are two template files in the root directory, that must be modified to include the appropriate files.

1. for main.tex, use \input to include each Latex file.

    \input{latex/<FILE>.tex}

2. for main.md, use the codeblock below to include each html files.

    ```{.include}
    html/<FILE>.html
    ``` 

Produce output

In the root directory, execute one of the following.

• make pdf to generate <MAIN>.pdf in the root directory
• make html to generate <MAIN>.html with supporting files in html/.
• make to execute both of the above
• make clean to remove all log files
• make clean_html to remove all generated html files
• make clean_pdf to remove all generated pdf files

Write markdown

Write markdown as usual. Mix in LaTeX by writing `some latex stuff`{=tex}. A more comprehensive list of what is supported can be found in Markdown references, including material on Citations.

The project uses pandoc for transpiling, and supports all features of pandoc markdown. The syntax is further extended by some Lua filters in this project. Here are some features that you might find useful:

Include Agda code

There are three ways to mix Agda code with other literate parts.

• Code blocks are enclosed in triple backticks.

```
_+_ : ℕ → ℕ → ℕ
zero + n = n
(suc m) + n = suc (m + n)
```

The Agda processor will type check the code and colour it appropriately.

• Displays start with four whitespaces. (In a markdown list, at least eight whitespaces are required.)

     0       + n  ≡  n
     (1 + m) + n  ≡  1 + (m + n)

Display code is not executed by the Agda processor and is not coloured.

• Inline code fragments are surrounded by single backticks.

The constructors for `ℕ` are `zero` and `suc`.

Inline code is not executed by the Agda processor and is not coloured.

For details, see the Agda documentation.

Mixing Latex and markdown

It is possible to write LaTeX mixed with markdown using pandoc tex blocks, which are ignored when generating html. Dually, markdown blocks are ignored when generating tex.

`This will be ignored by HTML`{=tex}
`and this will be ignored by LaTex`{=markdown}

For details, see the raw_tex section in pandoc markdown.

Citations

You could write LaTeX citation commands \cite{} and \shortcite{} directly in markdown source files. For example,

Applications of parametricity to functional programming are given by Wadler \shortcite{wadler_1989}

will be rendered as

Applications of parametricity to functional programming are given by Wadler \shortcite{wadler_1989}

in LaTeX and

Applications of parametricity to functional programming are given by Wadler [-@wadler_1989]

in the markdown path to HTML.

Specifying a bibliography

For HTML to render the citation, specify the location of bib files in the YAML header of the source file:

---
bibliography: references.bib
---

Body

For LaTeX, use \bibliography{references} in <MAIN>.tex, after \input and before \end{document}

Citation styles

For HTML, by default pandoc will use a Chicago author-date format for citations and references. To use another style, you will need to specify a CSL 1.0 style file in the csl metadata field. For example:

---
title: "Sample Document"
bibliography: references.bib
csl: journal-of-the-acm.csl
---

A primer on creating and modifying CSL styles is here, a repository of CSL styles is here, and an easily browsed list of styles is here.

For LaTeX, in main.tex, specify the name of a .bst file with the \bibiographystyle command. For example,

\bibliographystyle{ACM-Reference-Format}

Other YAML header options

Other options could be used, such as

• link-citations to make citations hyperlinked to their corresponding bibliography entries.
• reference-section-title to add a section header title before the bibliography.

---
link-citations: true
reference-section-title: References          
bibliography: references.bib
---

A list of header options appears on the pandoc citeproc man page.

Parts of this section are adapted from the citation section of the R markdown documentation.

Fenced div blocks

You may define your own LaTeX blocks by writing at least 3 consecutive colons plus some attributes. The attributes will become HTML classes and ids when generating HTML, and LaTeX commands if you define a mapping in your YAML header. This feature is supported by pandoc-latex-environment.

---                           
pandoc-latex-environment:
  center: [center]
---

:::{.center}
some content
:::

will be rendered in LaTeX as

\begin{center}
some content
\end{center}

and in HTML as

<div class="center">
some content
</div>

Tikz diagrams

Draw diagrams using the LaTeX package tikz-cd. For HTML the diagrams will be rendered as SVG files under html/tikz-diagrams.

```{=latex}
\begin{tikzcd}[column sep=5em,row sep=tiny]
  \blue{P~a} \arrow[r, "a≐b P" WildStrawberry] \arrow[dddd, "R a"' WildStrawberry]
& \blue{P~b} \arrow[dddd, "R~b" WildStrawberry]
\\~\\~\\~\\
  \blue{P'~a} \arrow[r, "a≐b P'" WildStrawberry]
& \blue{P'~b}
\end{tikzcd}
```

If you want to include your own LaTeX commands or packages, see the explanation of Pandoc Lua filters.

Customizing the LaTeX template

The important lines are:

\usepackage{fontspec}
\setmonofont[Scale=0.9]{DejaVu mononoki Symbola Droid}

and

\newfontfamily{\AgdaSerifFont}{Dejavu Serif}
\newfontfamily{\AgdaSansSerifFont}{DejaVu Sans}
\newfontfamily{\AgdaTypewriterFont}{DejaVu mononoki Symbola Droid}
\renewcommand{\AgdaFontStyle}[1]{{\AgdaSansSerifFont{}#1}}
\renewcommand{\AgdaKeywordFontStyle}[1]{{\AgdaSansSerifFont{}#1}}
\renewcommand{\AgdaStringFontStyle}[1]{{\AgdaTypewriterFont{}#1}}
\renewcommand{\AgdaCommentFontStyle}[1]{{\AgdaTypewriterFont{}#1}}
\renewcommand{\AgdaBoundFontStyle}[1]{\textit{\AgdaSansSerifFont{}#1}

They set up the correct fonts, which are crucial for rendering Unicode symbols.

Customizing the HTML template

Include header CSS in main.md header using:

---
header-includes: |
  <style>
  .center{
	  text-align:center;
  }
  </style>
---

Use together with fenced div blocks for styling HTML pages.

Pandoc Lua filters

Pandoc enables most of the document transformation. It parses source files into pandoc abstract syntax trees (ASTs) and writes them to another format. Pandoc filters allow the ASTs to be manipulated between the parsing and the writing phase.

The tool provides a collection of filters under pandoc-filters/. For example:

• tikz.lua transforms raw_latex blocks of tikz-cd into svg images. Adapted from pandoc lua-filter, this filter transforms tikz-cd commands in LaTeX to SVG images. It does this by rendering the code to pdf first, then using pdf2svg for outputting SVG. Changing the local variable tikz_doc_template will affect the look of the images.
• include-files.lua supports ```{.include} blocks.
• rewrite-html-links.lua rewrites links from included files. Pandoc processes file <file>.md to produce <file>.html. Within the latter, crosslinks have the form <file>.html#12345, and the Lau code rewrites these to <main>.html#12345 so they work correctly after the produced html is included into <main>.html.
• codeblocks.lua translates lagda markdown with three ticks to LaTeX {code} enviroments.
• citations-tex.lua transforms LaTeX citations in markdown, so they can be later translated to HTML

Possible future work

• improve tikz.lua to be more flexible (use preambles in markdown?)
• better dependency management and incorporation with pandoc and Agda