Alectryon 2.0

Version 2.0.0

• Alectryon is now compatible with Rocq 9, Docutils 22, Sphinx 9.1, Pygments 2.19, and Python 3.9+.

• Alectryon now supports the two main Rocq LSP servers: VsRocq and coq-lsp. VsRocq is the default for Rocq files, replacing SerAPI; it is reasonably well supported. Coq-lsp is experimental. SerAPI is still supported for Coq versions < 9. Known limitations are documented in VsRocq issues #1198, #1199, #1201, #1203, #1204, #1205, #1206, #1209, and #1210; help is welcome to fix these issues and improve VsRocq support (for now, Alectryon bundles mitigation for most of them). [ffffc91, 9ff1e75, c28fb38, 81dcd0a, 830f41e, 8c4f256]

• Settings from _RocqProject files are now recognized and applied. This makes it easy to configure dependencies (-Q …), warnings (-arg -w -arg -notation-for-abbreviation), printing parameters (-arg -set -arg "'Printing Depth=30'", -arg -set -arg "'Printing Width=55'"), etc.

• Alectryon now has experimental support for Dafny, including a literate-programming mode (conversions between Dafny files with /// comments and reST/Markdown documents) and semantic highlighting via the Dafny LSP server. [1f8370e, ca1b078, 6bdcd55]

• Alectryon now supports literate programming in Markdown in addition to reStructuredText. Markdown files (.md, .myst) containing {coq} code blocks can be rendered to LaTeX or HTML through Docutils, or converted to Rocq files (.v) with (*| … |*) comments using the coq backend, and vice versa using the coq+md frontend. [e17fe93, 46f037b, c5253aa, 8563218, 901247d]

• HTML and LaTeX files containing Rocq snippets can now be ingested by Alectryon and rewritten to insert recorded goals and prover outputs, using the new html and latex frontends. This makes it possible to process code blocks embedded in HTML or LaTeX documents without going through Docutils. [cc16941, 49f7ec1]

• alectryon-mode now supports Dafny, Lean 4, and markdown-mode buffers. [cf948f9, b7313ae, 32f0e1e, bec2575]

• Exporting to LaTeX now displays hypotheses bodies in addition to hypothesis types. [3456a60, d1f827c]

• A noop driver is now available for all languages, skipping prover execution entirely. [929066a]

Bug fixes

• (HTML) Do not add an HTML4 xmlns attribute to HTML5 outputs. [fab5384]

• (LaTeX) Fix an incompatibility with the hyperref package by namespacing alectryon macros (\al{xyz} expands to alectryon@xyz). [716454d]

• (LaTeX export) Prevent narrow spaces in \alectryonInline{} macros from propagating to \begin{alectryon} environments. [76fc9e0]

• (LaTeX) Fix a compatibility issue with the longtable package. [b5c3bfb]

Breaking changes

• (CLI) Error messages from Rocq now include column information. [1fdcd00]

• (Rocq) The default Coq driver is now vsrocq (was sertop). SerAPI is still available using --coq-driver sertop. [81dcd0a]

• (Rocq) The coqdoc frontend now invokes rocq doc instead of coqdoc. [829fde4]

• (Rocq) The default printing width and depth are now determined by Rocq, not Alectryon. To recover the previous behavior, create a _RocqProject file with -arg -set -arg "'Printing Depth=30'" and -arg -set -arg "'Printing Width=55'".

• (Lean) The literate-programming comment delimiters for Lean files have changed from /-! … !-/ to /-| … |-/. [278fb59]

• (LaTeX) The alectryon and alectryon@inline environments have been simplified to make it easier to redefine them. [2be8328]

• (LaTeX) All Alectryon macros are now wrapped in \al / \Al commands (e.g., \al{xyz} expands to alectryon@xyz). [424709a]

• (HTML) The HTML class alectryon-wsp has been renamed to alectryon-txt. [872e83d]