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

Note: This package has metadata revisions in the cabal description newer than included in the tarball. To unpack the package including the revisions, use 'cabal get'.

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 && <0.18) [details]
Tested with ghc ==8.0.2, ghc ==8.2.2, ghc ==8.4.4, ghc ==8.6.5, ghc ==8.8.4, ghc ==8.10.4, ghc ==9.0.1
License LicenseRef-PublicDomain
Copyright Andreas Abel, 2020, 2021
Author Andreas Abel
Maintainer Andreas Abel <andreas.abel@cse.gu.se>
Revised Revision 1 made by AndreasAbel at 2023-06-09T15:44:19Z
Category Dependent types, Development
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.2021.6.1)
Uploaded by AndreasAbel at 2021-06-01T06:39:12Z
Distributions LTSHaskell:0.2023.6.9, NixOS:0.2023.6.9, Stackage:0.2023.6.9
Executables agda2lagda
Downloads 815 total (10 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 2021-06-01 [all 1 reports]

Readme for agda2lagda-0.2021.6.1

[back to package description]

Hackage version agda2lagda on Stackage Nightly Stackage LTS version Cabal build Stack build

agda2lagda: Convert Agda/Haskell text to literate Agda/Haskell text

Generate a LaTeX literate Agda/Haskell script from an Agda/Haskell script.

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

Examples (rendered):

Example: agda2lagda Foo.agda

Input: Foo.agda

-- Sample non-literate Agda program
-- ================================
--
-- A remark to test bulleted lists:
--
-- * This file serves as example for agda2lagda.
--
-- * The content may be non-sensical.
--
-- Indeed!

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

-- A subheading
---------------

module Submodule where

  postulate
    zeta : D

-- That's it.
-- Bye.

Output: Foo.lagda.tex

%% This file was automatically generated by agda2lagda 0.2021.6.1.

\heading{Sample non-literate Agda program}

A remark to test bulleted lists:

\begin{itemize}

\item
This file serves as example for agda2lagda.

\item
The content may be non-sensical.

\end{itemize}

Indeed!

\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
%% -- -}
%% --

\subheading{A subheading}

\begin{code}
module Submodule where

  postulate
    zeta : D
\end{code}

That's it.
Bye.

Installation

These are standard installation instructions.

Last update of installation instructions: 2021-05-29.

From stackage.org

Requires stack.

stack update
stack install agda2lagda

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.4, 9.0.1.