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

This is a package candidate release! Here you can preview how this package release will appear once published to the main package index (which can be accomplished via the 'maintain' link below). Please note that once a package has been published to the main package index it cannot be undone! Please consult the package uploading documentation for more information.

[maintain] [Publish]

Warnings:

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]

Properties

Versions 0.2020.11.1, 0.2021.6.1, 0.2023.1.12, 0.2023.3.25, 0.2023.6.9, 0.2023.6.9
Change log CHANGELOG.md
Dependencies base (>=4.9 && <5), directory, filepath, optparse-applicative (>=0.13) [details]
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-09T15:49:12Z

Downloads

Maintainer's Corner

Package maintainers

For package maintainers and hackage trustees


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):

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

Examples

Given input Foo.agda:

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.