Katla: LaTeX & HTML code listing generator for Idris2

Pre-alpha version. Interface might change as the command line interface generator library Collie evolves.

Dependencies:

• Idris2 downstream of PR#1941
• Installing the Idris 2 API
• Collie library for command line interfaces
• Idrall library for Dhall bindings

Usage

To generate a document, a corresponding ttm file is required along with the idr file. After a successful build, you will find them in build/ttc/{ttc_version}. ttc_version depends on your environment.

To generate an HTML:

$ katla html path/to/src/Foo.idr path/to/ttm/Foo.ttm > Foo.html

To generate a TeX file and a PDF:

$ katla latex path/to/src/Foo.idr path/to/ttm/Foo.ttm > Foo.tex
$ pdflatex Foo.tex

Generated TeX files may have dependencies. Currently, they require the following packages:

• inconsolata
• fancyvrb
• xcolor

You can investigate potential dependencies by searching the code:

$ grep usepackage src/Katla/LaTeX.idr

Active examples of using Katla can be found in the main repository of Idris2:
https://github.com/idris-lang/Idris2/blob/main/.github/scripts/katla.sh

Using katla-typst

To generate semantically highlighted typst documents from literate .typ files, build and invoke katla-typst:

$ katla-typst path/to/src/Foo.typ path/to/ttm/Foo.ttm > KFoo.typ

In order to use the output of the above command, you also need to append the output of katla-typst preamble to your template file:

$ katla-typst preamble >> my_template.typ

Demo

See example tests.

PRs welcome!

Wishlist:

• Error handling
• Batch mode
• Separate into a library + driver module (so we could write Idris programs that generate such sources)