agda2lagda

Translate .agda files into .lagda.tex files.

https://github.com/andreasabel/agda2lagda

LTS Haskell 20.15:0.2021.6.1
Stackage Nightly 2023-03-23:0.2023.1.12
Latest on Hackage:0.2023.1.12

See all snapshots agda2lagda appears in

LicenseRef-PublicDomain licensed by Andreas Abel
Maintained by Andreas Abel
This version can be pinned in stack with:agda2lagda-0.2023.1.12@sha256:05c9bb1df4a3c23214ed4fbd30608da03535142643a51e93e98864d8810b035d,4033

Module documentation for 0.2023.1.12

There are no documented modules for this package.

Hackage version agda2lagda on Stackage Nightly Stackage LTS version Cabal build Stack build

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.1.12"
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.1.12"
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.1.12

Installation from source

These are standard installation instructions.

Last update of installation instructions: 2023-01-11.

From stackage.org

Requires stack.

stack update
stack install agda2lagda

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.5, 9.4.4.

Changes

Revision history for agda2lagda

0.2023.1.12

  • New option --markdown producing .lagda.md files instead of .lagda.tex.
  • Tested with GHC 8.0.2 - 9.4.4.

0.2021.6.1

  • Paragraphs starting with * are recognized as \item and organized in an itemize environment. Cannot be nested.
  • Render doubly-underlined (===) paragraphs as \heading, dash-underlined (---) paragraphs as \subheading.
  • Added a small testsuite (cabal test) using goldplate.
  • Tested with GHC 8.10.4 and 9.0.1.

0.2020.11.1

  • First version. Released Halloween 2020.
  • Converts agda/hs files into lagda/lhs LaTeX literate files, turning line comments into text and block comments into LaTeX comments.
  • Tested with GHC 8.0.2 - 8.10.3.
A service provided by FP Complete