Skip to content

Alectryon 1.3.0
Compare
Choose a tag to compare
@cpitclaudel cpitclaudel released this 15 Aug 09:11
· 308 commits to master since this release
v1.3.0
This tag was signed with the committer’s verified signature.
cpitclaudel Clément Pit-Claudel
GPG key ID: D1FB5C3FD8E87699
Verified
Learn about vigilant mode.
c5441f3

Version 1.3.0

  • EXPERIMENTAL A new mini-language lets authors show or hide specific sentences, hypotheses, and goals within a fragment of Coq code. The same language can be used in conjunction with a new :mref: role to place markers and create references to a subpart of a goal, and with a new :mquote: role to replicate subparts of a goal inline. [8a02bce, 14f45b7, 4f91484] [GH-36, GH-2]

  • Alectryon's LaTeX preamble has been rewritten to improve line breaking between and within hypotheses. [3325d55]

  • .. coq:: directives now accept :class: and :name: arguments. [df6ff35, 7cf03d6]

  • A new --long-line-threshold flag controls the line length over which Alectryon will issue “long line” warnings. [0286051]

  • A new --cache-compression flag enables compression of generated cache files. This typically yields space savings of over 95%. [GH-35]

  • A new --html-minification flag enables the generation of more compact HTML files. Minified HTML files use backreferences to refer to repeated goals and hypotheses (these backreferences are resolved at display time using Javascript) and more succinct markup (full markup is rebuilt dynamically at page load). This typically saves 70-90% of the generated file size, and nearly as much on HTML generation time on page load times. [GH-35]

  • HTML5, XeLaTeX and LuaLaTeX outputs are now supported (--latex-dialect, --html-dialect). [c576ae8]

Bug fixes

  • Fix parsing of reST docinfo fields for custom highlighting (:alectryon/pygments/…:). [33df0f2]

Breaking changes

  • Improvements to goals rendering in HTML may cause very slight alignment changes. Use .alectryon-io .goal-separator { height: calc(1em + 1px); } to revert to the previous alignment (modulo rounding errors).

  • The LaTeX markup of hypotheses has changed: alectryon@hyp is now a macro, not an environment.

  • Docutils option "syntax_highlight" now defaults to "short" when using Alectryon's CLI or its custom HTML writer. That is, inline :coq: roles now produce short-form CSS Pygments class names when processed using alectryon.docutils or the CLI. [72749bd]

  • The HTML markup for alectryon-io blocks has been simplified to save space in generated files (may affect third-party stylesheets). Specifically, the .highlight class is now applied to whole .alectryon-io blocks; .hyp-body-block and .hyp-type-block are now .hyp-body and .hyp-type; and the following classes have been removed: .goal-hyp (use .goal-hyps > span), .hyp-name (use .goal-hyps var), .hyp-body (use .hyp-body > span), .hyp-type (use .hyp-type > span), .hyp-punct (use .goal-hyps b or .hyp-type > b and .hyp-body > b), .alectryon-output-stycky-wrapper (use .alectryon-output > div), .alectryon-extra-goal-label (use .alectryon-extra-goals > .goal-separator). [59563f1, dc4b128, 28a004e]

  • json.Cache in module alectryon.json now takes arbitrary metadata instead of sertop_args. [56ca103]

  • json_of_annotated and annotated_of_json in module alectryon.json are now PlainSerializer.encode and PlainSerializer.decode. [c1076cc]

Assets 2
Loading