agda2lagda
Translate .agda files into .lagda.tex files.
https://github.com/andreasabel/agda2lagda
LTS Haskell 22.43: | 0.2023.6.9 |
Stackage Nightly 2024-12-03: | 0.2023.6.9 |
Latest on Hackage: | 0.2023.6.9 |
agda2lagda-0.2023.6.9@sha256:8320e9e11c44bb3763963c0f9a979126125d930620ee37e097b2ad4dd6337c5e,2699
Module documentation for 0.2023.6.9
There are no documented modules for this package.
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
\heading
s. - Paragraphs followed by a line of dashes are turned into
\subheading
s. - Consecutive paragraphs starting
*
are turned into anitemize
environment. - 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
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 outputFoo.lagda.tex
. - Invocation
agda2lagda --markdown Foo.agda
produces 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 $< >> $@
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.
Changes
Revision history for agda2lagda
0.2023.6.9
West Pride revision.
- Builds with
optparse-applicative-0.18
. - Tested with GHC 8.0.2 - 9.6.2.
0.2023.3.25
- Output
-o
ending in.md
or.markdown
now activates--markdown
format. - Tested with GHC 8.0.2 - 9.6.1.
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 anitemize
environment. Cannot be nested. - Render doubly-underlined (
===
) paragraphs as\heading
, dash-underlined (---
) paragraphs as\subheading
. - Added a small testsuite (
cabal test
) usinggoldplate
. - Tested with GHC 8.10.4 and 9.0.1.
0.2020.11.1
- First version. Released Halloween 2020.
- Converts
.agda
and.hs
files into.lagda
or.lhs
LaTeX literate files, turning line comments into text and block comments into LaTeX comments. - Tested with GHC 8.0.2 - 8.10.3.