[tool] Pretty Print to HTML

[lemmy]

TLA+ has a great pretty-printer to TeX (tla2tex), but HTML is becoming a de-facto document standard, especially for content shared online. HTML also has other advantages, such as the ability to automatically add hyperlinks from symbols to their definitions, and allow for collapsing and expanding proofs. The existing tla2tex code already contains most of the necessary parsing and typesetting pre-processing (like alignment), and could serve as a basis for an HTML pretty-printer. A prototype already exists.

Copied from: https://github.com/tlaplus/tlaplus/blob/master/general/docs/contributions.md#pretty-print-to-html-difficulty-easy-skills-java-html. Originally proposed by @pron.

[xxyzzn]

HTML may be a de facto standard for displaying cat videos and their literary equivalents, but the de facto standard for displaying math and documents in many other scientific fields is pdf. And Web browsers display it. It may be possible to display math formulas decently in HTML, but not in any standard way; and I wouldn't know how to do it. (As near as I can tell MathHTML is dead.)

If you want to display TLA+ in HTML, you should display the ASCII version. And, as I recall, TLA+ users never look at the pretty-printed version anyway. It shouldn't be too hard to duplicate the appropriate features of the Toolbox editor (clicking to reach a symbol's definition/declaration and collapsing/expanding proofs) on an HTML page. In fact, that could become part of the front-end for a web-based Toolbox.

[muenchnerkindl]

For what it's worth, established proof assistants usually produce both HTML and PDF versions of logical theories. Whereas the PDFs tend to have good pretty-printing (through LaTeX), the HTMLs are more or less souped-up versions of the ASCII sources but include links to resources they depend on.

Examples:

• Isabelle colors keywords and has a poor man's pretty-printing of symbols within ASCII; it contains links to theories that the current theory depends on but not to operator definitions or lemmas used, cf. https://isabelle.in.tum.de/dist/library/HOL/HOL/Nat.html.
• Coq displays pure ASCII with keywords colored but has extensive links for all symbols, cf. https://coq.github.io/doc/master/stdlib/Coq.Arith.PeanoNat.html.
• Lean has links similar to Coq but with symbols rendered similarly to what Isabelle does and with more elaborate HTML / Javascript for exhibiting more structure in its display of theories, cf. https://leanprover-community.github.io/mathlib_docs/init/data/int/basic.html#int.

[pron]

HTML output can look pretty much identical to the PDF output, with the following benefits:

• Render in the browser (i.e. the page source contains the ASCII, and if JS is enabled it is pretty-printed, otherwise it is shown as ASCII).
• Copy to ASCII
• Links (definitions, proof steps)
• Hover-tooltips
• Proof-stage collapse/expansion

As a demonstration of what's possible, here's a screenshot of a prototype HTML pretty-printer output, that renders in the browser and has copy-as-ASCII.

[xxyzzn]

That looks pretty good. I have two questions: What are the odds that your html file will still work in 20 years? Is it easy to display a snippet of TLA+ or PlusCal inside an ordinary HTML document?

[pron]

What are the odds that your html file will still work in 20 years?

The file is just the ASCII representation and a link to the JS renderer, so it will work 100%, but might, in the worst-case show just the ASCII.

Is it easy to display a snippet of TLA+ or PlusCal inside an ordinary HTML document?

That would be the vision. My very partial POC required that any TLA+ block be a complete module.