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 or Haskell files into literate files. Single line comments are interpreted as text, the rest as code blocks.


[Skip to Readme]

Properties

Versions 0.2020.11.1, 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
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.2020.11.1)
Uploaded by AndreasAbel at 2020-10-31T23:53:43Z

Downloads

Maintainer's Corner

For package maintainers and hackage trustees


Readme for agda2lagda-0.2020.11.1

[back to package description]

Hackage version agda2lagda on Stackage Nightly Stackage LTS version Build Status

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

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

Example: agda2lagda Foo.agda

Input: Foo.agda

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

-- Another heading
------------------

module Submodule where

  postulate
    zeta : D

-- That's it.
-- Bye.
-- -} -} -} -}

Output: Foo.lagda.tex

\heading{Foo heading}

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

\heading{Another heading}

\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: 2020-11-01.

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