diff --git a/CHANGELOG.md b/CHANGELOG.md --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -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. diff --git a/Makefile b/Makefile --- a/Makefile +++ b/Makefile @@ -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 "" > $@ -# @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 "" > $@ +# # @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 diff --git a/README.md b/README.md --- a/README.md +++ b/README.md @@ -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. diff --git a/agda2lagda.cabal b/agda2lagda.cabal --- a/agda2lagda.cabal +++ b/agda2lagda.cabal @@ -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 -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 diff --git a/src/Options.hs b/src/Options.hs --- a/src/Options.hs +++ b/src/Options.hs @@ -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 diff --git a/test/golden/ClosingCommentInString.lagda.md b/test/golden/ClosingCommentInString.lagda.md --- a/test/golden/ClosingCommentInString.lagda.md +++ b/test/golden/ClosingCommentInString.lagda.md @@ -1,4 +1,4 @@ - + This demonstrates a known issue: The parser is not aware of strings, thus, diff --git a/test/golden/ClosingCommentInString.lagda.tex b/test/golden/ClosingCommentInString.lagda.tex --- a/test/golden/ClosingCommentInString.lagda.tex +++ b/test/golden/ClosingCommentInString.lagda.tex @@ -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, diff --git a/test/golden/Foo.lagda.md b/test/golden/Foo.lagda.md --- a/test/golden/Foo.lagda.md +++ b/test/golden/Foo.lagda.md @@ -1,4 +1,4 @@ - + Sample non-literate Agda program ================================ diff --git a/test/golden/Foo.lagda.tex b/test/golden/Foo.lagda.tex --- a/test/golden/Foo.lagda.tex +++ b/test/golden/Foo.lagda.tex @@ -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} diff --git a/test/markdown-infer-format.goldplate b/test/markdown-infer-format.goldplate new file mode 100644 --- /dev/null +++ b/test/markdown-infer-format.goldplate @@ -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" } + ] +}