Hackage :: [Package]

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

Maintainer's Corner

Package maintainers

For package maintainers and hackage trustees

Candidates

Versions [RSS] 0.2020.11.1, 0.2021.6.1, 0.2023.1.12, 0.2023.3.25, 0.2023.6.9
Change log CHANGELOG.md
Dependencies base (>=4.9 && <5), directory, filepath, optparse-applicative (>=0.13) [details]
Tested with ghc ==9.6.2, ghc ==9.4.5, 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-2023
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 2023-06-09T16:48:01Z
Distributions LTSHaskell:0.2023.6.9, NixOS:0.2023.6.9, Stackage:0.2023.6.9
Executables agda2lagda
Downloads 819 total (11 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 2023-06-09 [all 1 reports]

Readme for agda2lagda-0.2023.6.9

[back to package description]

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