agdatex

agdatex allows to extract reusable LaTeX-Macros from .agda-files annotated via comments.

Dependencies

Python >= 3.11

Annotations

The following comment annotations are supported:

--! NAME defines the \NAME LaTeX-macro for the Agda-code from the next line until the next empty line or EOF. Example:
```
--! example
ex : ℕ
ex = 0

foo : ℕ
foo = 1
```
Defines the \example macro, which includes ex but not foo.
--! NAME { defines the \NAME LaTeX-macro for the Agda-code from the next line until the --! } end annotation token. Example:
```
--! examples {
ex : ℕ
ex = 0

foo : ℕ
foo = 1
--! }
```
Defines the \examples macro, which includes ex and foo.
--! NAME > opens a namespace, i.e. all subsequent definitions will be prefixed with NAME. Namespaces can be nested. Example:
```
--! Example >

--! Ex
ex : ℕ
ex = 0

--! Foo
foo : ℕ
foo = 1
```
Defines the macros \ExampleEx and \ExampleFoo.
--! < closes a namespace. Namespaces are also automatically closed at the end of the file.
--!! NAME behaves like --! but the resulting macro typesets the code inline and not as a block.
--! [ hides code inside of a command.
--! ] stops hiding code inside of a command.

Usage

Let's say you have a project structure like

.
├── .git
├── agda.sty
├── main.tex
└── STLC
    ├── Properties.agda
    └── Syntax.agda

where STLC/Syntax.agda begins with

module STLC.Syntax where

Running

$ ./agdatex.py -o latex STLC/*.agda

has the following effect:

the project root is discovered by searching outwards until a .git directory is found;
the project root is copied to a fresh temp directory;
the copied STLC/*.agda-files are transpiled to *.lagda.tex-files;
agda is run with the LaTeX-backend on the *.lagda.tex-files;
the corresponding latex/STLC/*.tex files appear in the actual project root;
a latex/agda-generated.sty file is generated that \inputs all the generated STLC/*.tex files;
the temp directory is removed again.

The main.tex-file can then import all generated macros via \usepackage{agda-generated}.

Copying is necessary as Agda does not support having .lagda.tex- and .agda-files with the same name. Copying the entire project root allows the .agda-files, which should be converted to LaTeX, to dependent on the rest of the project.

For smaller projects without a .agda-lib-file, you might want to explicitly specify the root directory via the --root flag.

Complete Example

A complete example including a Makefile can be found in the example-subdirectory.

Manpage

Usage: agdatex [-h] [-o PATH] [-e PATH] [-t PATH] [-k] [-r PATH] [-i PATH] SRC_PATH [SRC_PATH ...]

Positional Arguments:

SRC_PATH Path to an annotated .agda-file.

Optional Arguments: