agda2lagda 0.2023.1.12 → 0.2023.3.25
raw patch · 10 files changed
+119/−66 lines, 10 files
Files
- CHANGELOG.md +10/−7
- Makefile +27/−17
- README.md +6/−6
- agda2lagda.cabal +24/−25
- src/Options.hs +37/−7
- test/golden/ClosingCommentInString.lagda.md +1/−1
- test/golden/ClosingCommentInString.lagda.tex +1/−1
- test/golden/Foo.lagda.md +1/−1
- test/golden/Foo.lagda.tex +1/−1
- test/markdown-infer-format.goldplate +11/−0
CHANGELOG.md view
@@ -1,5 +1,10 @@ # Revision history for agda2lagda +## 0.2023.3.25++* Output `-o` ending in `.md` or `.markdown` now activates `--markdown` format.+* Tested with GHC 8.0.2 - 9.6.1.+ ## 0.2023.1.12 * New option `--markdown` producing `.lagda.md` files instead of `.lagda.tex`.@@ -7,18 +12,16 @@ ## 0.2021.6.1 -* Paragraphs starting with `* ` are recognized as `\item` and- organized in an `itemize` environment. Cannot be nested.+* Paragraphs starting with `* ` are recognized as `\item` and organized in an `itemize` environment.+ Cannot be nested. * Render doubly-underlined (`===`) paragraphs as `\heading`, dash-underlined (`---`) paragraphs as `\subheading`.-* Added a small testsuite (`cabal test`) using- [`goldplate`](https://hackage.haskell.org/package/goldplate).+* Added a small testsuite (`cabal test`) using [`goldplate`](https://hackage.haskell.org/package/goldplate). * 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.+* Converts `.agda` and `.hs` files into `.lagda` or `.lhs` LaTeX literate files,+ turning line comments into text and block comments into LaTeX comments. * Tested with GHC 8.0.2 - 8.10.3.
Makefile view
@@ -1,48 +1,58 @@-.PHONY : bug haddock install quick-test test test-help version- expand-includes=data/expand-includes.awk +.PHONY: all all : test README.md -# Atm, hackage renders comments verbatim, so we need to delete them.-# https://github.com/haskell/hackage-server/issues/937-README.md : data/cpp.README.md $(expand-includes) Makefile- @echo "Regenerating $@."- @rm $@-# @echo "<!-- DO NOT EDIT me directly, as I am generated from $< ! -->" > $@-# @echo "" >> $@- @$(expand-includes) $< | strip-html-comments.sed >> $@+# OBSOLETE, hackage is fixed:+# # Atm, hackage renders comments verbatim, so we need to delete them.+# # https://github.com/haskell/hackage-server/issues/937+# README.md : data/cpp.README.md $(expand-includes) Makefile+# @echo "Regenerating $@."+# @rm $@+# # @echo "<!-- DO NOT EDIT me directly, as I am generated from $< ! -->" > $@+# # @echo "" >> $@+# @$(expand-includes) $< | strip-html-comments.sed >> $@ -test :+.PHONY: test+test: cabal test +.PHONY: accept fix-tests+accept: fix-tests fix-tests: cabal exec -- goldplate --fix test +.PHONY: test-help test-help: cabal run agda2lagda -- --help -version :+.PHONY: version+version: cabal run agda2lagda -- --version -quick-test :+.PHONY: quick-test+quick-test: cabal run agda2lagda -- -v --force -o test/out/ test/Foo.agda cabal run agda2lagda -- -v --force -o test/Foo-generated.lagda test/Foo.agda -bug :+.PHONY: bug+bug: cabal run agda2lagda -- --dry-run test/ClosingCommentInString.agda -install :+.PHONY: install+install: cabal install -haddock :+.PHONY: haddock+haddock: cabal v1-haddock --executables # To install bash completion, # agda2lagda needs to be installed on the PATH. # (Only needs to be installed once, even if options of agda2lagda change.) -install-bash-completion :+.PHONY: install-bash-completion+install-bash-completion: install-bash-completion.sh agda2lagda # EOF
README.md view
@@ -87,7 +87,7 @@ For example, under Linux (similar under macOS): ```shell-VERSION="0.2023.1.12"+VERSION="0.2023.3.25" SRC="https://github.com/andreasabel/agda2lagda/releases/download/v${VERSION}/agda2lagda-${VERSION}-linux.binary" TGT="/usr/local/bin/agda2lagda" wget ${SRC} -O ${TGT}@@ -95,7 +95,7 @@ ``` For macOS, there is also a installer package, e.g.: ```shell-VERSION="0.2023.1.12"+VERSION="0.2023.3.25" SRC="https://github.com/andreasabel/agda2lagda/releases/download/v${VERSION}/agda2lagda-${VERSION}-mac.pkg" TGT="/tmp/agda2lagda.pkg" wget ${SRC} -O ${TGT}@@ -106,7 +106,7 @@ $ which agda2lagda /usr/local/bin/agda2lagda $ agda2lagda --version-agda2lagda version 0.2023.1.12+agda2lagda version 0.2023.3.25 ``` Installation from source@@ -114,14 +114,14 @@ These are standard installation instructions. -Last update of installation instructions: 2023-01-11.+Last update of installation instructions: 2023-03-25. ### From stackage.org Requires [stack](https://docs.haskellstack.org/en/stable/install_and_upgrade/). ``` stack update-stack install agda2lagda+stack install agda2lagda --resolver nightly ``` ### From hackage.haskell.org@@ -152,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.7, 9.0.2, 9.2.5, 9.4.4.+8.0.2, 8.2.2, 8.4.4, 8.6.5, 8.8.4, 8.10.7, 9.0.2, 9.2.7, 9.4.4.
agda2lagda.cabal view
@@ -1,8 +1,7 @@-cabal-version: >=1.10--- NB: Cabal file initially generated by 'cabal init'.+cabal-version: 1.24 name: agda2lagda-version: 0.2023.1.12+version: 0.2023.3.25 synopsis: Translate .agda files into .lagda.tex files. description: Simple command line tool to convert plain Agda@@ -16,37 +15,37 @@ author: Andreas Abel maintainer: Andreas Abel <andreas.abel@cse.gu.se>-copyright: Andreas Abel, 2020, 2021, 2022+copyright: Andreas Abel, 2020-2023 category: Dependent types, Development build-type: Simple -extra-source-files: CHANGELOG.md- README.md- Makefile- test/*.goldplate- test/*.agda- test/golden/*.lagda.md- test/golden/*.lagda.tex+extra-doc-files:+ CHANGELOG.md+ README.md -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.7- GHC == 9.0.2- GHC == 9.2.5- GHC == 9.4.4+extra-source-files:+ Makefile+ test/*.goldplate+ test/*.agda+ test/golden/*.lagda.md+ test/golden/*.lagda.tex -source-repository head- type: git- location: git://github.com/andreasabel/agda2lagda.git+tested-with:+ GHC == 9.6.1+ GHC == 9.4.4+ GHC == 9.2.7+ GHC == 9.0.2+ GHC == 8.10.7+ GHC == 8.8.4+ GHC == 8.6.5+ GHC == 8.4.4+ GHC == 8.2.2+ GHC == 8.0.2 -source-repository this+source-repository head type: git location: git://github.com/andreasabel/agda2lagda.git- tag: v0.2023.1.12 executable agda2lagda main-is: Main.hs
src/Options.hs view
@@ -22,6 +22,8 @@ import Util import Version +-- import Debug.Trace (traceShowId)+ self :: String self = "agda2lagda" @@ -33,6 +35,22 @@ , (Markdown , ".lhs" ) ])) ] +-- | Map extensions to formats.+formatMap :: [(String, Format)]+formatMap =+ [ (".tex", LaTeX)+ , (".md", Markdown)+ , (".markdown", Markdown)+ ]++-- | From the name of the output file, determine the format.+formatFromFilename :: String -> Maybe Format+formatFromFilename file =+ case filter (\ (ext, _) -> ext `List.isSuffixOf` file) formatMap of+ -- Only determine format if we have exactly one hit+ [ (_, fmt) ] -> Just fmt+ _ -> Nothing+ -- | Format of the output. data Format = LaTeX -- ^ Latex literate text.@@ -57,15 +75,24 @@ { optVerbose :: Bool , optDryRun :: Bool , optForce :: Bool- , optFormat :: Format+ , optFormat :: Maybe Format -- , optLatex :: Bool -- , optMarkdown :: Bool , optOutput :: Maybe FilePath , optInput :: Maybe FilePath } deriving Show +inferFormatFromOutput :: Options -> Options+inferFormatFromOutput opts+ | Nothing <- optFormat opts, Just out <- optOutput opts = opts { optFormat = formatFromFilename out }+ | otherwise = opts++-- | Default format to 'LaTeX'.+getFormat :: Options -> Format+getFormat = fromMaybe LaTeX . optFormat+ options :: IO Options-options =+options = inferFormatFromOutput <$> do 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."@@ -75,6 +102,7 @@ versionOption = infoOption (unwords versionWords) $ long "version"+ <> short 'V' <> hidden <> help "Show version info." versionWords = concat@@ -118,7 +146,7 @@ <> help "Comment on what is happening." oFormat =- flag LaTeX Markdown+ flag Nothing (Just Markdown) $ long "markdown" <> help "Produce Markdown instead of LaTeX." @@ -147,7 +175,7 @@ <> short 'o' <> metavar "OUT" <> action "directory"- <> help "Name of output file or directory."+ <> help "Name of output file or directory. Ending '.md' or '.markdown' determines Markdown output." oStdin = flag' Nothing@@ -175,6 +203,7 @@ let o = show format in List.intercalate "\t" [ "", src, "--" ++ o ++ "-->", tgt ] , [ ""+ , "If the path OUT given via -o ends in '.md' or '.markdown', '--markdown' is assumed." , "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" ]@@ -212,22 +241,23 @@ | otherwise = " (only if output is not newer than input)" getTarget :: Options -> IO Target-getTarget Options{..} = do+getTarget opts@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)+ return (language, format, outFile) where+ format = getFormat opts -- 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+ ext <- lookup format rest Just (language, (base, ext)) addDir (Just (Dir dir)) = (dir </>) . takeFileName
test/golden/ClosingCommentInString.lagda.md view
@@ -1,4 +1,4 @@-<!-- This file was automatically generated by agda2lagda 0.2023.1.12. -->+<!-- This file was automatically generated by agda2lagda 0.2023.3.25. --> This demonstrates a known issue: The parser is not aware of strings, thus,
test/golden/ClosingCommentInString.lagda.tex view
@@ -1,4 +1,4 @@-%% This file was automatically generated by agda2lagda 0.2023.1.12.+%% This file was automatically generated by agda2lagda 0.2023.3.25. This demonstrates a known issue: The parser is not aware of strings, thus,
test/golden/Foo.lagda.md view
@@ -1,4 +1,4 @@-<!-- This file was automatically generated by agda2lagda 0.2023.1.12. -->+<!-- This file was automatically generated by agda2lagda 0.2023.3.25. --> Sample non-literate Agda program ================================
test/golden/Foo.lagda.tex view
@@ -1,4 +1,4 @@-%% This file was automatically generated by agda2lagda 0.2023.1.12.+%% This file was automatically generated by agda2lagda 0.2023.3.25. \heading{Sample non-literate Agda program}
+ test/markdown-infer-format.goldplate view
@@ -0,0 +1,11 @@+{ "command" : "agda2lagda"+, "input_files" : "Foo.agda"+, "arguments" : ["--verbose", "--output", "tmp-golden/${GOLDPLATE_INPUT_NAME}.lagda.md", "${GOLDPLATE_INPUT_FILE}"]+, "asserts" :+ [ { "exit_code" : 0 }+ , { "created_file" : "tmp-golden/${GOLDPLATE_INPUT_NAME}.lagda.md"+ , "contents" : "golden/${GOLDPLATE_INPUT_NAME}.lagda.md"+ }+ , { "created_directory" : "tmp-golden" }+ ]+}