# 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\; =\; \backslash pm\backslash 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.