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

[ dependent-types, development, program ] [ Propose Tags ]

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]
Versions [RSS] [faq] 0.2020.11.1, 0.2021.6.1
Change log CHANGELOG.md
Dependencies base (>=4.9 && <5), directory, filepath, optparse-applicative [details]
License LicenseRef-PublicDomain
Copyright Andreas Abel, 2020, 2021
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 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.2021.6.1, NixOS:0.2021.6.1, Stackage:0.2021.6.1
Executables agda2lagda
Downloads 208 total (13 in the last 30 days)
Rating (no votes yet) [estimated by Bayesian average]
Your Rating
  • λ
  • λ
  • λ
Status Hackage Matrix CI
Docs not available [build log]
Last success reported on 2021-06-01 [all 1 reports]

Downloads

Maintainer's Corner

For package maintainers and hackage trustees

Candidates


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

  • http://www.cse.chalmers.se/~abela/#MultiSortedAlgebra
  • http://www.cse.chalmers.se/~abela/#cr-sk

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.