agda2lagda 0.2021.6.1 → 0.2023.1.12
raw patch · 15 files changed
+577/−279 lines, 15 files
Files
- CHANGELOG.md +5/−0
- Makefile +3/−0
- README.md +76/−98
- agda2lagda.cabal +15/−7
- src/Main.hs +8/−171
- src/Markup.hs +1/−0
- src/Options.hs +243/−0
- src/Render.hs +20/−2
- src/Util.hs +2/−1
- test/golden/ClosingCommentInString.lagda.md +40/−0
- test/golden/ClosingCommentInString.lagda.tex +41/−0
- test/golden/Foo.lagda.md +50/−0
- test/golden/Foo.lagda.tex +55/−0
- test/markdown.goldplate +9/−0
- test/tests.goldplate +9/−0
CHANGELOG.md view
@@ -1,5 +1,10 @@ # Revision history for agda2lagda +## 0.2023.1.12++* New option `--markdown` producing `.lagda.md` files instead of `.lagda.tex`.+* Tested with GHC 8.0.2 - 9.4.4.+ ## 0.2021.6.1 * Paragraphs starting with `* ` are recognized as `\item` and
Makefile view
@@ -16,6 +16,9 @@ test : cabal test +fix-tests:+ cabal exec -- goldplate --fix test+ test-help: cabal run agda2lagda -- --help
README.md view
@@ -6,11 +6,17 @@ -agda2lagda: Convert Agda/Haskell text to literate Agda/Haskell text-===================================================================+agda2lagda: Convert program to literate program (Agda/Haskell)+============================================================== -Generate a LaTeX literate Agda/Haskell script from an Agda/Haskell script.+Generate a literate Agda/Haskell script from an Agda/Haskell script.+Produces LaTeX or Markdown literate scripts. +Specification+-------------++Conversion into LaTeX (default):+ - 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.@@ -23,120 +29,92 @@ - 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`-```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`-```latex-%% This file was automatically generated by agda2lagda 0.2021.6.1.--\heading{Sample non-literate Agda program}+Conversion into Markdown (option `--markdown`) is similar,+but nothing needs to be done for headings and itemize environments: -A remark to test bulleted lists:+- Single line comments are turned into ordinary text.+ * At the end of the file, extra block comment terminators are removed. -\begin{itemize}+- Comment blocks, if started on the 0th column, count as _commenting out_.+ These will be turned into HTML comments.+ Nested comments are not recognized. -\item-This file serves as example for agda2lagda.+- The rest is interpreted as code and wrapped in a code environment (triple backticks). -\item-The content may be non-sensical.+Examples+-------- -\end{itemize}+Given input [`Foo.agda`](https://github.com/andreasabel/agda2lagda/blob/master/test/Foo.agda):+- Invocation `agda2lagda Foo.agda` produces output+ [`Foo.lagda.tex`](https://github.com/andreasabel/agda2lagda/blob/master/test/golden/Foo.lagda.tex).+- Invocation `agda2lagda --markdown Foo.agda` produces output+ [`Foo.lagda.md`](https://github.com/andreasabel/agda2lagda/blob/master/test/golden/Foo.lagda.md). -Indeed!+LaTeX examples (rendered):+- http://www.cse.chalmers.se/~abela/#MultiSortedAlgebra+- http://www.cse.chalmers.se/~abela/#cr-sk -\begin{code}-module Foo where-\end{code}+Example `Makefile` to turn `.agda` file into highlighted HTML via Markdown (since `v0.2023.1.12`):+```make+FILE=Foo+TITLE=The Title -Some data type.+default : md/html/$(FILE).html -\begin{code}-data D : Set where- c : D-\end{code}+# Step 1: agda2lagda: Produce Markdown literate script. -A function.+md/%.lagda.md : %.agda+ agda2lagda -f --markdown -o md/ $< -\begin{code}-foo : D → D-foo c = c -- basically, the identity-\end{code}+# Step 2: agda: Highlight and format code blocks as HTML.+# Also produces Agda.css. -%% This part is commented out.-%% {--%% bar : D → Set-%% bar x = D-%% -- -}-%% --+md/html/%.md : md/%.lagda.md+ cd md ; agda --html --html-highlight=auto ../$< -\subheading{A subheading}+# Step 3: pandoc: Produce HTML. Improvise header to make HTML self-contained. -\begin{code}-module Submodule where+md/html/%.html : md/html/%.md+ echo '<!DOCTYPE HTML><html><head><meta charset="utf-8"><title>$(TITLE)</title><link rel="stylesheet" href="Agda.css"></head>' > $@+ pandoc -f markdown -t html $< >> $@+``` - postulate- zeta : D-\end{code}+Installation from binary+------------------------ -That's it.-Bye.+Binaries for Linux, macOS and Windows are available from [GitHub releases](https://github.com/andreasabel/agda2lagda/releases).+Just download the executable for your platform there and put it in a directory that is in the system `PATH`. +For example, under Linux (similar under macOS):+```shell+VERSION="0.2023.1.12"+SRC="https://github.com/andreasabel/agda2lagda/releases/download/v${VERSION}/agda2lagda-${VERSION}-linux.binary"+TGT="/usr/local/bin/agda2lagda"+wget ${SRC} -O ${TGT}+chmod +x ${TGT} ```+For macOS, there is also a installer package, e.g.:+```shell+VERSION="0.2023.1.12"+SRC="https://github.com/andreasabel/agda2lagda/releases/download/v${VERSION}/agda2lagda-${VERSION}-mac.pkg"+TGT="/tmp/agda2lagda.pkg"+wget ${SRC} -O ${TGT}+open ${TGT}+```+Verify the installation with these commands (Linux/macOS):+```console+$ which agda2lagda+/usr/local/bin/agda2lagda+$ agda2lagda --version+agda2lagda version 0.2023.1.12+``` -## Installation+Installation from source+------------------------ These are standard installation instructions. -Last update of installation instructions: 2021-05-29.+Last update of installation instructions: 2023-01-11. ### From stackage.org @@ -162,9 +140,9 @@ 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:+E.g. if you have GHC 8.10.7 installed, you can use this compiler as follows: ```-stack install --system-ghc --stack-yaml stack-8.10.2.yaml+stack install --system-ghc --stack-yaml stack-8.10.7.yaml ``` Alternatively, `stack` can install the compiler for you: ```@@ -174,4 +152,4 @@ 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.+8.0.2, 8.2.2, 8.4.4, 8.6.5, 8.8.4, 8.10.7, 9.0.2, 9.2.5, 9.4.4.
agda2lagda.cabal view
@@ -2,7 +2,7 @@ -- NB: Cabal file initially generated by 'cabal init'. name: agda2lagda-version: 0.2021.6.1+version: 0.2023.1.12 synopsis: Translate .agda files into .lagda.tex files. description: Simple command line tool to convert plain Agda@@ -16,7 +16,7 @@ author: Andreas Abel maintainer: Andreas Abel <andreas.abel@cse.gu.se>-copyright: Andreas Abel, 2020, 2021+copyright: Andreas Abel, 2020, 2021, 2022 category: Dependent types, Development build-type: Simple@@ -24,16 +24,20 @@ extra-source-files: CHANGELOG.md README.md Makefile- test/Foo.agda- test/ClosingCommentInString.agda+ test/*.goldplate+ test/*.agda+ test/golden/*.lagda.md+ test/golden/*.lagda.tex 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+ GHC == 8.10.7+ GHC == 9.0.2+ GHC == 9.2.5+ GHC == 9.4.4 source-repository head type: git@@ -42,13 +46,14 @@ source-repository this type: git location: git://github.com/andreasabel/agda2lagda.git- tag: v0.2021.6.1+ tag: v0.2023.1.12 executable agda2lagda main-is: Main.hs other-modules: LexicalStructure Markup+ Options Render Util Version@@ -94,6 +99,7 @@ -- TypeSynonymInstances ghc-options: -Wall+ -Wcompat -Wno-missing-pattern-synonym-signatures test-suite test@@ -106,3 +112,5 @@ -- goldplate requires ghc >= 8.4 , process build-tool-depends: goldplate:goldplate+ -- We also need to depend on ourselves since goldplate calls us.+ , agda2lagda:agda2lagda
src/Main.hs view
@@ -11,39 +11,23 @@ module Main where import Control.Monad-import qualified Data.List as List-import Data.Semigroup -import Options.Applicative-import Options.Applicative.Help.Pretty (vcat, text) -- , (<$$>))--import System.Directory (doesFileExist, doesDirectoryExist, createDirectoryIfMissing)-import System.FilePath- (splitExtension, addExtension, takeFileName, takeDirectory, hasTrailingPathSeparator, (</>))+import System.Directory (doesFileExist, createDirectoryIfMissing)+import System.FilePath (takeDirectory) import System.IO (hPutStr, stderr) import System.Exit (exitFailure) import LexicalStructure+import Options import Render-import Util ((<&>))-import Version -self :: String-self = "agda2lagda"--extensionMap :: [(String,String)]-extensionMap =- [ (".agda" , ".lagda.tex")- , (".hs" , ".lhs")- ]- main :: IO () main = do -- Parse options. opts@Options{..} <- options- target <- getTarget opts+ target@(language, format, mout) <- getTarget opts chat opts $ vocalizeOptions opts target -- Parse input.@@ -53,12 +37,14 @@ -- Generate output. - let result = lagdaTex items+ let result = case format of+ LaTeX -> lagdaTex items+ Markdown -> lagdaMd language items -- Save to file or print to stdout. chat opts $ "Writing output...\n"- case target of+ case mout of Nothing -> putStr result Just outFile -> do @@ -79,155 +65,6 @@ -- Done. chat opts $ unwords [ self, "terminated successfully.\n" ]---- * Option parsing and handling--data Options = Options- { optVerbose :: Bool- , optDryRun :: Bool- , optForce :: Bool- , optOutput :: Maybe FilePath- , optInput :: Maybe FilePath- } deriving Show--options :: IO Options-options =- execParser $- info (helper <*> versionOption <*> numericVersionOption <*> programOptions)- (header "Translates Agda/Haskell text into literate Agda/Haskell text, turning line comments into ordinary text and code into TeX code blocks."- <> footerDoc (Just foot))-- where- versionOption =- infoOption (unwords versionWords)- $ long "version"- <> help "Show version info."- versionWords = concat- [ [ self, "version", version ]- , [ "(Halloween edition)" | ".11.1" `List.isSuffixOf` version ]- ]-- numericVersionOption =- infoOption version- $ long "numeric-version"- <> help "Show just version number."- -- Newline at the end:- -- <> helpDoc (Just $ text "Show just version number." <$$> text "")-- programOptions = Options- <$> oVerbose- <*> oDryRun- <*> oForce- <*> oOutput- <*> (oStdin <|> oInput)-- oForce =- switch- $ long "force"- <> short 'f'- <> help "Overwrite existing output files."-- oDryRun =- switch- $ long "dry-run"- <> help "Do not write any output files, write to standard output."-- oVerbose =- switch- $ long "verbose"- <> short 'v'- <> help "Comment on what is happening."-- oOutput =- optional $ strOption- $ long "output"- <> short 'o'- <> metavar "OUT"- <> action "directory"- <> help "Name of output file or directory."-- oStdin =- flag' Nothing- $ long "stdin"- <> help "Read from standard input."-- oInput :: Parser (Maybe FilePath)- oInput = dashToStdin <$> do- strArgument- $ metavar "INFILE"- <> action "file"- <> help "The input file containing the Agda/Haskell text."- where- -- dash is interpreted as stdin- dashToStdin = \case- "-" -> Nothing- file -> Just file-- foot = vcat $ map text $ concat- [ [ "Unless explicitly given via -o, the name of the output file is computed by replacing the extension of the input file, according to the following rules:"- , "" ]- , flip map extensionMap $ \ (src, tgt) ->- List.intercalate "\t" [ "", src, "-->", tgt ]- , [ ""- , "If the path OUT given via -o is a directory, that's where the output file will be placed."- , ""- , unwords [ "Example:", self, "path/to/file.agda" ]- , ""- , "This will write file path/to/file.lagda.tex unless it already exists."- , "To overwrite existing files, use option -f."- , ""- , unwords [ "Example:", self, "path/to/file.hs", "-o out/dir" ]- , ""- , "This places the output in file out/dir/file.lhs."- , ""- , unwords [ "Example:", self, "path/to/file.hs", "-o new/dir/" ]- , ""- , "This places the output in file new/dir/file.lhs, creating directories new/ and new/dir/ if necessary."- ]- ]--type Target = Maybe FilePath--vocalizeOptions :: Options -> Target -> String-vocalizeOptions Options{..} target = unlines $ map concat- [ [ "Plan:" ]- , [ "- Read from "- , maybe "standard input" ("file " ++) optInput- , "."- ]- , [ "- Write to "- , maybe "standard output" (\ f -> "file " ++ f ++ unlessNewer) target- , "."- ]- ]- where- unlessNewer- | optForce = ""- | otherwise = " (only if output is not newer than input)"--getTarget :: Options -> IO Target-getTarget Options{..}- | optDryRun = return Nothing- | otherwise = traverse dirOrFile optOutput <&> \ mout ->- if | Just (File out) <- mout -> Just out- | Just inp <- optInput ->- case splitExtension inp of- (base, src) | Just tgt <- lookup src extensionMap- -> Just $ addDir mout $ addExtension base tgt- _ -> Nothing- | otherwise -> Nothing- where- addDir (Just (Dir dir)) = (dir </>) . takeFileName- addDir _ = id--data DirOrFile = Dir FilePath | File FilePath--dirOrFile :: FilePath -> IO DirOrFile-dirOrFile path- | hasTrailingPathSeparator path = return $ Dir path- | otherwise = doesDirectoryExist path <&> \case- True -> Dir path- False -> File path chat :: Options -> String -> IO () chat o msg = when (optVerbose o) $ hPutStr stderr msg
src/Markup.hs view
@@ -5,6 +5,7 @@ module Markup ( markup, Item(..), TextItem(..)+ , gobbleTrailingBlockCommentClosers ) where import Util
+ src/Options.hs view
@@ -0,0 +1,243 @@+module Options+ ( Options(..)+ , options+ , Format(..)+ , Language(..)+ , languageToHighlighter+ , getTarget+ , self+ , vocalizeOptions+ )+ where++import qualified Data.List as List++import Options.Applicative+import Options.Applicative.Help.Pretty (vcat, text) -- , (<$$>))++import System.Directory (doesDirectoryExist)+import System.FilePath+ (splitExtension, addExtension, takeFileName, hasTrailingPathSeparator, (</>))++import Util+import Version++self :: String+self = "agda2lagda"++extensionMap :: [(String,(Language,[(Format,String)]))]+extensionMap =+ [ (".agda" , (Agda , [ (LaTeX , ".lagda.tex")+ , (Markdown , ".lagda.md" ) ]))+ , (".hs" , (Haskell , [ (LaTeX , ".lhs" )+ , (Markdown , ".lhs" ) ]))+ ]++-- | Format of the output.+data Format+ = LaTeX -- ^ Latex literate text.+ | Markdown -- ^ Markdown literate text.+ deriving (Eq, Show)++-- formatToLongOption :: Format -> String+-- formatToLongOption = map toLower . show++data Language+ = Agda+ | Haskell+ deriving (Eq, Show)++-- | Get markdown highlighter identifier (e.g. "agda", "haskell") for language.+languageToHighlighter :: Language -> String+languageToHighlighter = map toLower . show++-- * Option parsing and handling++data Options = Options+ { optVerbose :: Bool+ , optDryRun :: Bool+ , optForce :: Bool+ , optFormat :: Format+ -- , optLatex :: Bool+ -- , optMarkdown :: Bool+ , optOutput :: Maybe FilePath+ , optInput :: Maybe FilePath+ } deriving Show++options :: IO Options+options =+ execParser $+ info (helper <*> versionOption <*> numericVersionOption <*> programOptions)+ (header "Translates Agda/Haskell text into literate Agda/Haskell text, turning line comments into ordinary text and code into TeX code blocks."+ <> footerDoc (Just foot))++ where+ versionOption =+ infoOption (unwords versionWords)+ $ long "version"+ <> hidden+ <> help "Show version info."+ versionWords = concat+ [ [ self, "version", version ]+ , [ "(Halloween edition)" | ".11.1" `List.isSuffixOf` version ]+ ]++ numericVersionOption =+ infoOption version+ $ long "numeric-version"+ <> hidden+ <> help "Show just version number."+ -- Newline at the end:+ -- <> helpDoc (Just $ text "Show just version number." <$$> text "")++ programOptions = Options+ <$> oVerbose+ <*> oDryRun+ <*> oForce+ <*> oFormat+ <*> oOutput+ <*> (oStdin <|> oInput)++ oForce =+ switch+ $ long "force"+ <> short 'f'+ <> help "Overwrite existing output files."++ oDryRun =+ switch+ $ long "dry-run"+ <> hidden+ <> help "Do not write any output files, write to standard output."++ oVerbose =+ switch+ $ long "verbose"+ <> short 'v'+ <> hidden+ <> help "Comment on what is happening."++ oFormat =+ flag LaTeX Markdown+ $ long "markdown"+ <> help "Produce Markdown instead of LaTeX."++ -- oLaTeX =+ -- switch+ -- $ long (formatToLongOption LaTeX)+ -- <> help (concat ["Generate LaTeX (default if --", formatToLongOption Markdown, " is not given)."])++ -- oMarkdown =+ -- switch+ -- $ long (formatToLongOption Markdown)+ -- <> help "Generate Markdown (possibly inferred from OUT file extension)."++ -- oLaTeX =+ -- optional $ strOption+ -- $ long "latex"+ -- <> value ""+ -- <> noArgError (ShowHelpText Nothing)+ -- <> metavar "LATEXFILE"+ -- <> action "file"+ -- <> help "Generate LaTeX (if LATEXFILE is not given, it is computed from INFILE and OUT)."++ oOutput =+ optional $ strOption+ $ long "output"+ <> short 'o'+ <> metavar "OUT"+ <> action "directory"+ <> help "Name of output file or directory."++ oStdin =+ flag' Nothing+ $ long "stdin"+ <> help "Read from standard input."++ oInput :: Parser (Maybe FilePath)+ oInput = dashToStdin <$> do+ strArgument+ $ metavar "INFILE"+ <> action "file"+ <> help "The input file containing the Agda/Haskell text."+ where+ -- dash is interpreted as stdin+ dashToStdin = \case+ "-" -> Nothing+ file -> Just file++ foot = vcat $ map text $ concat+ [ [ "Unless explicitly given via -o, the name of the output file is computed by replacing the extension of the input file, according to the following rules:"+ , "" ]+ , extensionMap >>= \ (src, (_language, rest)) ->+ rest <&> \ (format, tgt) ->+ -- let o = "--" ++ formatToLongOption format ++ ":" in+ let o = show format in+ List.intercalate "\t" [ "", src, "--" ++ o ++ "-->", tgt ]+ , [ ""+ , "If the path OUT given via -o is a directory, that's where the output file will be placed."+ , ""+ , unwords [ "Example:", self, "path/to/file.agda" ]+ , ""+ , "This will write file path/to/file.lagda.tex unless it already exists."+ , "To overwrite existing files, use option -f."+ , ""+ , unwords [ "Example:", self, "path/to/file.hs", "-o out/dir" ]+ , ""+ , "This places the output in file out/dir/file.lhs."+ , ""+ , unwords [ "Example:", self, "path/to/file.hs", "-o new/dir/" ]+ , ""+ , "This places the output in file new/dir/file.lhs, creating directories new/ and new/dir/ if necessary."+ ]+ ]++type Target = (Language, Format, Maybe FilePath)++vocalizeOptions :: Options -> Target -> String+vocalizeOptions Options{..} (language, format, target) = unlines $ map concat+ [ [ "Plan:" ]+ , [ "- Read " ++ show language ++ " code from "+ , maybe "standard input" ("file " ++) optInput+ , "."+ ]+ , [ "- Write " ++ show format ++ " to "+ , maybe "standard output" (\ f -> "file " ++ f ++ unlessNewer) target+ , "."+ ]+ ]+ where+ unlessNewer+ | optForce = ""+ | otherwise = " (only if output is not newer than input)"++getTarget :: Options -> IO Target+getTarget Options{..} = do+ let language = maybe Agda fst m+ outFile <- if optDryRun then return Nothing else do+ traverse dirOrFile optOutput <&> \ mout ->+ if | Just (File out) <- mout -> Just out+ | Just (_, (base, tgt)) <- m -> Just $ addDir mout $ addExtension base tgt+ | otherwise -> Nothing+ return (language, optFormat, outFile)+ where+ -- Resolve Language, basename, and extension from input file.+ m :: Maybe (Language, (FilePath, FilePath))+ m = do+ inp <- optInput+ let (base, src) = splitExtension inp+ (language, rest) <- lookup src extensionMap+ ext <- lookup optFormat rest+ Just (language, (base, ext))++ addDir (Just (Dir dir)) = (dir </>) . takeFileName+ addDir _ = id++data DirOrFile = Dir FilePath | File FilePath++dirOrFile :: FilePath -> IO DirOrFile+dirOrFile path+ | hasTrailingPathSeparator path = return $ Dir path+ | otherwise = doesDirectoryExist path <&> \case+ True -> Dir path+ False -> File path
src/Render.hs view
@@ -5,11 +5,11 @@ module Render ( lagdaTex+ , lagdaMd ) where -import Util- import qualified LexicalStructure as L+import Options (Language, languageToHighlighter) import Markup import Version @@ -43,3 +43,21 @@ , map (unlines . ("\\item" :)) ps , [ "\\end{itemize}" ] ]++-- | Render into literate Markdown Agda.++lagdaMd :: Language -> [L.Item] -> String+lagdaMd language its = unlines $ concat+ [ ["<!-- This file was automatically generated by agda2lagda " ++ version ++ ". -->"]+ , [""]+ , map render $ gobbleTrailingBlockCommentClosers its+ ]+ where+ render = \case+ L.TextItem s -> s+ L.CommItem s -> unwords ["<!--", s, "-->"]+ L.CodeItem s -> concat+ [ "```" ++ languageToHighlighter language ++ "\n"+ , s+ , "```\n"+ ]
src/Util.hs view
@@ -3,10 +3,11 @@ module Util (module Util, module X) where import Data.Bifunctor as X-import Data.Char as X (isSpace)+import Data.Char as X (isSpace, toLower) import Data.Function as X (on) import Data.List as X (dropWhileEnd, groupBy) import Data.Maybe as X+import Data.Semigroup as X (<&>) :: Functor f => f a -> (a -> b) -> f b (<&>) = flip (<$>)
+ test/golden/ClosingCommentInString.lagda.md view
@@ -0,0 +1,40 @@+<!-- This file was automatically generated by agda2lagda 0.2023.1.12. -->++This demonstrates a known issue:+The parser is not aware of strings, thus,+a closing block comment delimiter inside a string+is taken as a closing block comment delimiter.++Without nested comments:++<!-- This is commented-out.+test = "A weird string with comment closing+ -->+```agda+ and other garbage @#$% that appears now as Agda code!"+-}+```++With nested comments:++<!-- +{- This is commented-out.+test = "A weird string with comment closing -} and other garbage @#$%!"+-- NB: this confuses even Agda (at the time of writing, version 2.6.1).+ -->+```agda+This should be still commented-out. -}+```++The reverse situation:++```agda+test = "Never put comment opening {- inside a string!"++postulate+ ThisShouldNotBeCommentedOut : Set++-- -} This should be text, not code!!+```++SNAFU.
+ test/golden/ClosingCommentInString.lagda.tex view
@@ -0,0 +1,41 @@+%% This file was automatically generated by agda2lagda 0.2023.1.12.++This demonstrates a known issue:+The parser is not aware of strings, thus,+a closing block comment delimiter inside a string+is taken as a closing block comment delimiter.++Without nested comments:++%% This is commented-out.+%% test = "A weird string with comment closing++\begin{code}+ and other garbage @#$% that appears now as Agda code!"+-}+\end{code}++With nested comments:++%% +%% {- This is commented-out.+%% test = "A weird string with comment closing -} and other garbage @#$%!"+%% -- NB: this confuses even Agda (at the time of writing, version 2.6.1).++\begin{code}+This should be still commented-out. -}+\end{code}++The reverse situation:++\begin{code}+test = "Never put comment opening {- inside a string!"++postulate+ ThisShouldNotBeCommentedOut : Set++-- -} This should be text, not code!!+\end{code}++SNAFU.+
+ test/golden/Foo.lagda.md view
@@ -0,0 +1,50 @@+<!-- This file was automatically generated by agda2lagda 0.2023.1.12. -->++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!++```agda+module Foo where+```++Some data type.++```agda+data D : Set where+ c : D+```++A function.++```agda+foo : D → D+foo c = c -- basically, the identity+```++<!-- This part is commented out.+{-+bar : D → Set+bar x = D+-- -}+--+ -->+A subheading+-------------++```agda+module Submodule where++ postulate+ zeta : D+```++That's it.+Bye.
+ test/golden/Foo.lagda.tex view
@@ -0,0 +1,55 @@+%% This file was automatically generated by agda2lagda 0.2023.1.12.++\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.+
+ test/markdown.goldplate view
@@ -0,0 +1,9 @@+{+ "command": "agda2lagda",+ "input_files": "*.agda",+ "arguments": ["--dry-run", "--markdown", "${GOLDPLATE_INPUT_FILE}"],+ "asserts": [+ {"exit_code": 0},+ {"stdout": "golden/${GOLDPLATE_INPUT_NAME}.lagda.md"}+ ]+}
+ test/tests.goldplate view
@@ -0,0 +1,9 @@+{+ "command": "agda2lagda",+ "input_files": "*.agda",+ "arguments": ["--dry-run", "${GOLDPLATE_INPUT_FILE}"],+ "asserts": [+ {"exit_code": 0},+ {"stdout": "golden/${GOLDPLATE_INPUT_NAME}.lagda.tex"}+ ]+}