Alectryon 1.4.0

Version 1.4.0

• JSON recordings (produced by --backend json) can now be used as inputs to generate webpages or highlighted snippets. [c69b08e]

• Alectryon's cache format has changed to support documents with multiple languages. Caches created with previous versions of Alectryon can still be read and do not need to be regenerated. [d376077]

• Alectryon can now compile Coq documents without running proofs nor recording Coq's output. This is useful for quick experimentation. [GH-52] [6f4ae20]

• Alectryon can now compile Coq documents with coqc instead of SerAPI. The results do not include goals or messages. This is useful when trying out a version of Coq that SerAPI does not support yet. [GH-60] [735e72b]

• Per-document Coq syntax-highlighting rules added to the docinfo section at the beginning of each document are now prefixed with alectryon/pygments/coq/ instead of alectryon/pygments/ (the legacy prefix is still supported). [3a9ffe6]

• A new extension of the marker-placement mini-language allows authors to attach properties to parts of a proof; for example, .. coq:: .s(Extraction).msg[lang]=haskell highlights all messages produced by Extraction commands using the Haskell lexer instead of the usual Coq lexer. [409fa6c]

• A new massert directive silently provides a simple form of unit-testing by silently checking a collection of marker-placement references, thus confirming that the prover's output matches user-provided search patterns. [bc2d8a4] [GH-63]

• A new mquote directive complements the mquote role by allowing authors to quote parts of a proof as a block (the mquote role generates inline text). [e0c9eda]

• Alectryon now accepts a --pygments-style flag to chose which Pygments code-highlighting style to use. It also honors the Sphinx configuration option pygments_style. [GH-58] [63539ed]

• Alectryon now exits with an informative error code (10 + the level of the most severe Docutils error). [GH-57] [dffde22]

Breaking changes

• Multiple APIs have been generalized to allow working with languages other than Coq and drivers other than SerAPI. In particular, docutils.AlectryonTransform.SERTOP_ARGS is now docutils.AlectryonTransform.DRIVER_ARGS['sertop'] [735e72b]; transforms.DEFAULT_TRANSFORMS is now transforms.DEFAULT_TRANSFORMS["coq"] [370b820]; docinfo headers for custom highlighting now use the prefix alectryon/pygments/coq/ instead of alectryon/pygments/ [a58a044] (backwards-compatible); caches are now partitioned by language [d376077] (backwards-compatible); html.gen_banner now takes a list of DriverInfo instances (renamed from GeneratorInfo in [2ce6c0a]) instead of a single one [d376077]; --backend json now writes files named .v.io.json instead of .io.json; and --frontend json is now --frontend coq.json [] (backwards-compatible).

• SerAPI-specific parts of the core module have been moved to a new serapi module. [91058a6]

• The Pygments stylesheets generated by Alectryon were renamed from tango_subtle.sty and tango_subtle.css to pygments.sty and pygments.css to reflect the fact that the style is not hardcoded any more. [9c15544] Instead, these stylesheets are now generated dynamically based on the style chosen using the --pygments-style flag or the pygments_style option in docutils.conf. [63539ed] The files assets/tango_subtle.* have been removed. [cea4ed4]

Bug fixes

• Alectryon will now copy assets (CSS and STY files) in the directory of the output file (rather than that of the input file) when no --output-directory is specified. This only matters if an output file is specified using -o (otherwise, the directory of the output file is the same as the input file, so the new behavior matches the old one). [6a35af2]