		Search-engine friendly clone of the ACL2 documentation.

Xdoc

Katex-integration

Support for LaTeX-like typesetting of mathematics in XDOC topics. (experimental)

Experimental. This whole thing is experimental. Jared reserves the right to decide it is a bad idea and remove support for it.

The Khan Academy has developed a very nice Javascript library, KaTeX, for rendering mathematical formulas in the web browser. We have now integrated KaTeX into XDOC's fancy web-based viewer, allowing you to typeset basic formulas.

Basic Usage

ESCAPING WARNING. LaTeX-style formulas may be especially hard to type in ordinary ACL2 string literals because you have to escape all the backslashes. For instance, you have to remember to write \\sqrt{x} instead of \sqrt{x}. You can avoid this headache by using the ACL2::fancy-string-reader. In the rest of this document, we will use the concrete xdoc syntax without the escapes for simplicity.

To typeset block-style formulas, you can use the @([...]) preprocessor directive, e.g.,:

@([
   c = \pm\sqrt{a^2 + b^2}
])

Produces an indented block of mathematics:

c = \pm\sqrt{a^2 + b^2}

You can also write inline math using @($...$) directive, for instance:

The product @($a \times b$) is even.

Produces text such as: the product a \times b.

Tips and Tricks

Fast Preview.

The KaTeX Preview page lets you interactively type in your formula and see how it will be typeset. It may be especially helpful since KaTeX only supports a particular subset of LaTeX.

Invalid Formulas.

Invalid formulas will display as an ugly error message. For instance, here is an invalid @([ ... ]) style formula:

{ there is no closing brace

And here is an invalid @($...$) style formula, { there is no closing brace , embedded in a paragraph.

Miscellaneous Notes

The preprocessor directives expand into <math> and <mathfrag> tags. But you will probably want to stick to the preprocessor syntax, rather than directly using <math> tags, because if you try to use raw <math> tags then you have to remember to escape XML characters like < with <, which just isn't very readable.

All of this is fundamentally limited to the web-based viewer. It seems very unlikely that <math> formulas will ever look nice when shown at the terminal with :doc or in the ACL2-Doc Emacs viewer.