Skip to content

Latest commit

 

History

History
154 lines (114 loc) · 7.11 KB

mathjax.rst

File metadata and controls

154 lines (114 loc) · 7.11 KB
Raw

Using MathJax with Alectryon

This example shows how to combine Alectryon with MathJax. We'll do a pretty-printed version of the proof that \sum_{i = 0}^n i = \frac{n \cdot (n + 1)}{2}. Use the following command to compile it:

alectryon mathjax.rst # reST → HTML; produces ‘mathjax.html’

First, we start with a definition of sum:

.. coq::

   Require Import Coq.Unicode.Utf8. (* .none *)
   Require Import PeanoNat ArithRing.

   Fixpoint nsum max f :=
     match max with
     | O => f 0
     | S max' => f max + nsum max' f
     end.

Then, we add notations to print LaTeX code (this is only one way to do it; another way would be to parse Coq's output to reconstruct LaTeX):

.. coq::

   Notation "'\ccNat{}'" := nat.
   Notation "'\ccSucc{' n '}'" := (S n).
   Infix "\times" := mult
     (at level 30).
   Notation "'\ccNsum{' x '}{' max '}{' f '}'" :=
     (nsum max (fun x => f))
       (format "'\ccNsum{' x '}{' max '}{' f '}'").
   Notation "\ccNot{ x }" := (not x)
     (at level 100).
   Infix "\wedge" := and
     (at level 190, right associativity).
   Notation "A \Rightarrow{} B" := (∀ (_ : A), B)
     (at level 200, right associativity).
   Notation "'\ccForall{' x .. y '}{' P '}'" := (∀ x, .. (∀ y, P) ..)
     (at level 200, x binder, y binder, right associativity,
      format "'\ccForall{' x .. y '}{' P '}'").

Then, we add MathJax definitions for each of these custom macros (look at the page source to see them):

\(\newcommand{\ccQ}{\mathbb{Q}}\) \(\newcommand{\ccNat}{\mathbb{N}}\) \(\newcommand{\ccSucc}[1]{\mathrm{S}\:#1}\) \(\newcommand{\ccFrac}[2]{\frac{#1}{#2}}\) \(\newcommand{\ccPow}[2]{{#1}^{#2}}\) \(\newcommand{\ccNot}[1]{{\lnot #1}}\) \(\newcommand{\ccEvar}[1]{\textit{\texttt{#1}}}\) \(\newcommand{\ccForall}[2]{\forall \: #1. \; #2}\) \(\newcommand{\ccNsum}[3]{\sum_{#1 = 0}^{#2} #3}\)

Then we set up MathJax to render the proofs properly (look at the page source to see the relevant script):

/* Override MathJax margins */ .coq-math .goal-conclusion > *, .coq-math .hyp-body span > *, .coq-math .hyp-type span > * { margin: 0 !important; }

And finally we write the actual proofs:

.. coq::
   :class: coq-math

   Lemma Gauss: ∀ n,
       2 * (nsum n (fun i => i)) = n * (n + 1).
     induction n; cbn [nsum].
     - (* n ← 0 *)
       reflexivity.
     - (* n ← S _ *)
       rewrite Nat.mul_add_distr_l.
       rewrite IHn.
       ring.
   Qed.

Configuring MathJax

MathJax needs to be configured before it is loaded. This makes configuring it particularly tricky when you don't have full control on the generated webpage.

  • If you're using Docutils directly through Alectryon's command line, MathJax is loaded with the defer flag, so you can include a <script> block with your MathJax config anywhere in the document: use a .. raw:: html directive, like this:

    .. raw:: html

   <script type="text/javascript">
     MathJax = { options: { … } };
   </script>

  • If you're using Sphinx, MathJax is loaded with the async flag (see this issue), so there's a race condition and you can't depend on your configuration being processed early: you need to move the config to a separate file, or use the mathjax3_config option of Sphinx if does enough for your needs. See the tricks in recipes/sphinx/conf.py.

  • For other processors like Pelican, you need to either move your configuration to a separate file and make sure that it is loaded first, as in Sphinx, or find a way to defer MathJax. The following usually works:

    from docutils.writers._html_base import HTMLTranslator
HTMLTranslator.mathjax_script = '<script type="text/javascript" defer src="%s"></script>\n'

Additional notes and background

Instead of adding explicit mathjax_process classes on each math element, you might want to use the processHtmlClass option of MathJax. This is more complicated, but here's the process in a nutshell.

  1. Configure MathJax to stop ignoring <pre> blocks by adding a MathJax = … config block:

    MathJax = {}
MathJax.options = { processHtmlClass: 'mathjax_process|alectryon-io' };

  2. Add \( … \) math markers to tell MathJax where to look:

    MathJax.startup = {
    pageReady: function () {
        // … Custom code to add \( … \) delimiters
        return MathJax.startup.defaultPageReady(); // Then run MathJax
    }
}

  3. Ensure that these definitions are processed before MathJax itself is loaded, since it's not easy to reconfigure MathJax after loading it. Concretely, this means either adding defer to the MathJax <script> tag, moving the configuration to a separate script loaded before MathJax, or moving the MathJax <script> to the end of the file (past the configuration above).

    The problem is that docutils automatically inserts the MathJax <script> tag for you if you use some math in the document, so you don't have much control over it (if you don't have any :math: roles then there's no problem: you can include the MathJax script yourself as explained in the previous section).

Alectryon already configures docutils to load MathJax with the defer option, so the steps above should work reliably when using Alectryon in standalone mode (point [3.] is already taken care of).

Sphinx loads MathJax in async mode by default, so the above won't work reliably, and the mathjax3_config option is not always enough (it does not let you customize the pageReady function; see Sphinx issue 9450). Instead, put the configuration above in a separate script and include it in html_js_files with sufficiently low priority (must be < 500). See sphinx/conf.py and sphinx/_static/mathjax_config.js for an example (you can also inline the body of the script directly in conf.py).