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]

Simple command line tool to convert plain Agda files into literate files. Single line comments are interpreted as text, the rest as code blocks.


[Skip to Readme]

Properties

Versions 0.2020.9.30, 0.2020.11.1, 0.2021.6.1
Change log CHANGELOG.md
Dependencies ansi-wl-pprint, base (>=4.9 && <5), directory, filepath, optparse-applicative [details]
License LicenseRef-PublicDomain
Copyright Andreas Abel, 2020
Author Andreas Abel
Maintainer Andreas Abel <andreas.abel@cse.gu.se>
Category Dependent types
Home page https://github.com/andreasabel/agda2lagda
Bug tracker https://github.com/andreasabel/agda2lagda/issues
Source repo head: git clone git://github.com/andreasabel/agda2lagda.git
this: git clone git://github.com/andreasabel/agda2lagda.git(tag v0.2020.9.30)
Uploaded by AndreasAbel at 2020-10-01T12:26:15Z

Downloads

Maintainer's Corner

For package maintainers and hackage trustees


Readme for agda2lagda-0.2020.9.30

[back to package description]

agda2lagda: Convert Agda text to literate Agda text

Generate a LaTeX literate Agda script from an Agda script.

Example: agda2lagda Foo.agda

Input: Foo.agda

-- Sample non-literate Agda program.
--
-- This file serves as example for agda2lagda.
-- The content may be non-sensical.

module Foo where

-- Some data type.

data D : Set where
  c : D

-- A function.
foo : D → D
foo c = c   -- basically, the identity

{- This part is commented out.
{-
bar : D → Set
bar x = D
-- -}
-- -}

module Submodule where

  postulate
    zeta : D

-- That's it.
-- Bye.

Output: Foo.lagda.tex

Sample non-literate Agda program.

This file serves as example for agda2lagda.
The content may be non-sensical.

\begin{code}
module Foo where
\end{code}

Some data type.

\begin{code}
data D : Set where
  c : D
\end{code}

A function.

\begin{code}
foo : D → D
foo c = c   -- basically, the identity
\end{code}

%% This part is commented out.
%% {-
%% bar : D → Set
%% bar x = D
%% -- -}
%% --

\begin{code}
module Submodule where

  postulate
    zeta : D
\end{code}

That's it.
Bye.

Installation

Last update of installation instructions: 2020-09-30.

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.2 installed, you can use this compiler as follows:

stack install --system-ghc --stack-yaml stack-8.10.2.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.2.

Known bugs

Strings containing the closing comment delimiter "-}" confuse the lexer and may produce unexpected output. At the time of writing, this is already a problem in Agda, see https://github.com/agda/agda/issues/4953.