agda2lagda: Translate .agda files into .lagda.tex files.

[ dependent-types, development, program ] [ Propose Tags ] [ Report a vulnerability ]

Simple command line tool to convert plain Agda or Haskell files into literate files. Line comments are interpreted as text, the rest as code blocks.

[Skip to Readme]

Downloads

agda2lagda-0.2025.9.5.tar.gz [browse] (Cabal source package)
Package description (as included in the package)

Maintainer's Corner

Package maintainers

AndreasAbel

For package maintainers and hackage trustees

edit package information

Candidates

0.2020.9.30, 0.2020.11.1, 0.2021.6.1, 0.2023.1.11, 0.2023.1.12, 0.2023.3.25, 0.2023.6.9, 0.2025.9.5

Versions [RSS]	0.2020.11.1, 0.2021.6.1, 0.2023.1.12, 0.2023.3.25, 0.2023.6.9, 0.2025.9.5
Change log	CHANGELOG.md
Dependencies	base (>=4.9 && <5), directory, filepath, optparse-applicative (>=0.13) [details]
Tested with	ghc ==9.14.1, ghc ==9.12.2, ghc ==9.10.2, ghc ==9.8.4, ghc ==9.6.7, ghc ==9.4.8, ghc ==9.2.8, ghc ==9.0.2, ghc ==8.10.7, ghc ==8.8.4, ghc ==8.6.5, ghc ==8.4.4, ghc ==8.2.2, ghc ==8.0.2
License	LicenseRef-PublicDomain
Copyright	Andreas Abel, 2020-2025
Author	Andreas Abel
Maintainer	Andreas Abel <andreas.abel@cse.gu.se>
Category	Dependent types, Development
Home page	https://github.com/andreasabel/agda2lagda
Bug tracker	https://github.com/andreasabel/agda2lagda/issues
Source repo	head: git clone https://github.com/andreasabel/agda2lagda.git
Uploaded	by AndreasAbel at 2025-09-05T08:56:01Z
Distributions	LTSHaskell:0.2023.6.9, NixOS:0.2023.6.9, Stackage:0.2025.9.5
Executables	agda2lagda
Downloads	1009 total (26 in the last 30 days)
Rating	(no votes yet) [estimated by Bayesian average]
Your Rating	λ λ λ
Status	Docs not available [build log] Last success reported on 2025-09-05 [all 1 reports]

Readme for agda2lagda-0.2025.9.5

[back to package description]

agda2lagda: Convert program to literate program (Agda/Haskell)

Generate a literate Agda/Haskell script from an Agda/Haskell script. Produces LaTeX or Markdown literate scripts.

Specification

Conversion into LaTeX (default):

Single line comments are turned into ordinary LaTeX.
- Paragraphs followed by a line of equal signs are turned into \headings.
- Paragraphs followed by a line of dashes are turned into \subheadings.
- Consecutive paragraphs starting * are turned into an itemize environment.
- At the end of the file, extra block comment terminators are removed.
Comment blocks, if started on the 0th column, count as commenting out. These will be turned into TeX comments. Nested comments are not recognized.
The rest is interpreted as code and wrapped in a code environment.

Conversion into Markdown (option --markdown) is similar, but nothing needs to be done for headings and itemize environments:

Single line comments are turned into ordinary text.
- At the end of the file, extra block comment terminators are removed.
Comment blocks, if started on the 0th column, count as commenting out. These will be turned into HTML comments. Nested comments are not recognized.
The rest is interpreted as code and wrapped in a code environment (triple backticks).

Examples

Given input Foo.agda:

Invocation agda2lagda Foo.agda produces output Foo.lagda.tex.
Invocation agda2lagda --markdown Foo.agda produces output Foo.lagda.md.

LaTeX examples (rendered):

Example Makefile to turn .agda file into highlighted HTML via Markdown (since v0.2023.1.12):

FILE=Foo TITLE=The Title default : md/html/$(FILE).html # Step 1: agda2lagda: Produce Markdown literate script. md/%.lagda.md : %.agda	agda2lagda -f --markdown -o md/ $< # Step 2: agda: Highlight and format code blocks as HTML. # Also produces Agda.css. md/html/%.md : md/%.lagda.md	cd md ; agda --html --html-highlight=auto ../$< # Step 3: pandoc: Produce HTML. Improvise header to make HTML self-contained. md/html/%.html : md/html/%.md	echo '<!DOCTYPE HTML><html><head><meta charset="utf-8"><title>$(TITLE)</title><link rel="stylesheet" href="Agda.css"></head>' > $@	pandoc -f markdown -t html $< >> $@

Installation from binary

Binaries for Linux, macOS and Windows are available from GitHub releases. Just download the executable for your platform there and put it in a directory that is in the system PATH.

For example, under Linux (similar under macOS):

VERSION="0.2023.3.25" SRC="https://github.com/andreasabel/agda2lagda/releases/download/v${VERSION}/agda2lagda-${VERSION}-linux.binary" TGT="/usr/local/bin/agda2lagda" wget ${SRC} -O ${TGT} chmod +x ${TGT}

For macOS, there is also a installer package, e.g.:

VERSION="0.2023.3.25" SRC="https://github.com/andreasabel/agda2lagda/releases/download/v${VERSION}/agda2lagda-${VERSION}-mac.pkg" TGT="/tmp/agda2lagda.pkg" wget ${SRC} -O ${TGT} open ${TGT}

Verify the installation with these commands (Linux/macOS):

$ which agda2lagda /usr/local/bin/agda2lagda $ agda2lagda --version agda2lagda version 0.2023.3.25

Installation from source

These are standard installation instructions.

Last update of installation instructions: 2023-03-25.

From stackage.org

Requires stack.

stack update stack install agda2lagda --resolver nightly

From hackage.haskell.org

Requires GHC >= 8.0 and the Haskell Cabal.

cabal update cabal install agda2lagda

From the repository

git clone https://github.com/andreasabel/agda2lagda.git cd agda2lagda cabal install

Alternatively to the last line, you can use stack. E.g. if you have GHC 8.10.7 installed, you can use this compiler as follows:

stack install --system-ghc --stack-yaml stack-8.10.7.yaml

Alternatively, stack can install the compiler for you:

stack install --stack-yaml stack-xx.yy.zz.yaml

The xx.yy.zz is a placeholder for the GHC version, choose one (for which there is a .yaml file).

At the time of writing, installation with these GHC versions has been tested: 8.0.2, 8.2.2, 8.4.4, 8.6.5, 8.8.4, 8.10.7, 9.0.2, 9.2.7, 9.4.4.