agda2lagda
Translate .agda files into .lagda.tex files.
https://github.com/andreasabel/agda2lagda
Version on this page: | 0.2021.6.1 |
LTS Haskell 22.43: | 0.2023.6.9 |
Stackage Nightly 2024-12-05: | 0.2023.6.9 |
Latest on Hackage: | 0.2023.6.9 |
agda2lagda-0.2021.6.1@sha256:3c2c693da221196b69eaa188e5d99e39a8c9ad624716f04e8186e031cec41ec5,3690
Module documentation for 0.2021.6.1
There are no documented modules for this package.
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
\heading
s. - Paragraphs followed by a line of dashes are turned into
\subheading
s. - Consecutive paragraphs starting
*
are turned into anitemize
environment. - At the end of the file, extra block comment terminators are removed.
- Paragraphs followed by a line of equal signs are turned into
-
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.
Changes
Revision history for agda2lagda
0.2021.6.1
- Paragraphs starting with
*
are recognized as\item
and organized in anitemize
environment. Cannot be nested. - Render doubly-underlined (
===
) paragraphs as\heading
, dash-underlined (---
) paragraphs as\subheading
. - Added a small testsuite (
cabal test
) usinggoldplate
. - Tested with GHC 8.10.4 and 9.0.1.
0.2020.11.1
- First version. Released Halloween 2020.
- Converts agda/hs files into lagda/lhs LaTeX literate files, turning line comments into text and block comments into LaTeX comments.
- Tested with GHC 8.0.2 - 8.10.3.