Generate a literate Agda/Haskell script from an Agda/Haskell script. Produces LaTeX or Markdown literate scripts.
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 anitemizeenvironment. - At the end of the file, extra block comment terminators are removed.
- Paragraphs followed by a line of equal signs are turned into
-
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
codeenvironment.
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).
Given input Foo.agda:
- Invocation
agda2lagda Foo.agdaproduces outputFoo.lagda.tex. - Invocation
agda2lagda --markdown Foo.agdaproduces outputFoo.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 $< >> $@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.25These are standard installation instructions.
Last update of installation instructions: 2023-03-25.
Requires stack.
stack update
stack install agda2lagda --resolver nightly
Requires GHC >= 8.0 and the Haskell Cabal.
cabal update
cabal install agda2lagda
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.