bussproofs not correctly computed [Unicode kerning problem?]

[Jean-Luc-Picard-2021]

Issue Summary

I am using Math Jax 3 with bussproofs. The problem is observable for example in the Chrome browser.

Boundaries of the SVG box are not correctly computed leading to problems like:

• uncorrect page width centering
• and missing horizontal scroll bar.

Steps to Reproduce:

1. Use Math Jax 3 with bussproofs:

beginning of the HTML document:

<script>
    window.MathJax = {
        loader: {load: ['[tex]/bussproofs']},
        tex: {packages: {'[+]': ['bussproofs']}}
    };
</script>

end of the HTML document:

<script type="text/javascript" id="MathJax-script" async
        src="https://cdn.jsdelivr.net/npm/mathjax@3/es5/tex-svg.js">
</script>

JavaScript call when the plain content has been rendered:

   MathJax.typeset();

2. This is the second step

Create a small example:

\begin{prooftree}\AxiomC{}
\RightLabel{Ax}\UnaryInfC{p ⊢ p}
\RightLabel{I→}\UnaryInfC{ ⊢ p → p}
\end{prooftree}

Create a larger example:

\begin{prooftree}\AxiomC{}
\RightLabel{Ax}\UnaryInfC{p ⊢ p}
\AxiomC{}
\RightLabel{Ax}\UnaryInfC{¬p ⊢ ¬p}
\RightLabel{E→}\BinaryInfC{¬p, p ⊢ ⊥}
\RightLabel{I→}\UnaryInfC{¬p, p ⊢ ¬ ¬q}
\RightLabel{DNE}\UnaryInfC{¬p, p ⊢ q}
\RightLabel{I→}\UnaryInfC{¬p ⊢ p → q}
\AxiomC{}
\RightLabel{Ax}\UnaryInfC{(p → q) → p ⊢ (p → q) → p}
\RightLabel{E→}\BinaryInfC{(p → q) → p, ¬p ⊢ p}
\AxiomC{}
\RightLabel{Ax}\UnaryInfC{p ⊢ p}
\AxiomC{}
\RightLabel{Ax}\UnaryInfC{¬p ⊢ ¬p}
\RightLabel{E→}\BinaryInfC{¬p, p ⊢ ⊥}
\RightLabel{I→}\UnaryInfC{¬p ⊢ ¬p}
\RightLabel{E→}\BinaryInfC{¬p, (p → q) → p ⊢ ⊥}
\RightLabel{I→}\UnaryInfC{(p → q) → p ⊢ ¬ ¬p}
\RightLabel{DNE}\UnaryInfC{(p → q) → p ⊢ p}
\RightLabel{I→}\UnaryInfC{ ⊢ ((p → q) → p) → p}
\end{prooftree}

3. Further steps, etc.

The smaller example has an Ok bounding box:

The larger example has a not Ok bounding box:

Technical details:

See intro and steps.

Supporting information:

You can try it online: https://www.xlog.ch/runtab/doclet/docs/06_demo/wilson/example42/package.html

[Jean-Luc-Picard-2021]

I suspect it has to do with the kerning of the plain Unicode code points I was using. I find a similar problem elsewhere where a kerning problem with plain Unicode code

points is better seen. Whats the work around?

Math Jax 3 input:

\begin{prooftree}\AxiomC{}
\RightLabel{Ax}\UnaryInfC{φ ⊢ φ}
\RightLabel{R→}\UnaryInfC{ ⊢ φ → ψ, φ}
\AxiomC{}
\RightLabel{Ax}\UnaryInfC{φ ⊢ φ}
\RightLabel{R→}\UnaryInfC{ ⊢ φ → ψ, φ}
\RightLabel{L→}\BinaryInfC{χ → ψ ⊢ φ → ψ, φ}
\RightLabel{R→}\UnaryInfC{ ⊢ (χ → ψ) → φ → ψ, φ}
\AxiomC{}
\RightLabel{Ax}\UnaryInfC{χ ⊢ χ}
\AxiomC{}
\RightLabel{Ax}\UnaryInfC{ψ ⊢ ψ}
\RightLabel{R→}\UnaryInfC{ψ ⊢ φ → ψ}
\RightLabel{L→}\BinaryInfC{χ → ψ, χ ⊢ φ → ψ}
\RightLabel{R→}\UnaryInfC{χ ⊢ (χ → ψ) → φ → ψ}
\RightLabel{L→}\BinaryInfC{φ → χ ⊢ (χ → ψ) → φ → ψ}
\RightLabel{R→}\UnaryInfC{ ⊢ (φ → χ) → (χ → ψ) → φ → ψ}
\end{prooftree}

Math Jax 3 rendering:

[dpvc]

Your "kerning" issue is actually a different problem. It is a bug in the v3 SVG output when characters are used that aren't in the default MathJax TeX fonts. In this case, it is because upright Greek letters are not in the MathJax TeX fonts, and so that is triggering the bug. The bug is fixed in v4 (currently out in beta release). If you control the website that is displaying the results, you could switch to that. But if you are using a website like the one you link to for the example at the bottom of your original post, then your only choice to deal with the "kerning" problem is to switch to CHTML output using the MathJax contextual menu.

The centering/scroll-bar problem you originally reported is a different problem, however. The bussproofs macros are not correctly computing the full width of the expression, and are leaving the width giving the incorrect bounding box in your image above. I do not currently have a work-around for that. We will have to look into it further.

[zorkow]

As @dpvc mentioned, the issue you are seeing is that we are working with a lot of negative spacing to compute the size of the inference bars and centering of conclusions. This has an effect on the bounding boxes that are generally assumed to be smaller than the actual element they contains.

There are some improvements around bounding box computation in version 4. While they are not specific to bussproofs, they might still be helpful for you. Please give it a go.

E.g., here is a difference between bounding boxes I can observe between MJ3 and MJ4 in the a11y explorer. Let me know if switching to MJ4 does make a difference for you.

[Jean-Luc-Picard-2021]

Would it be adviseable to split off the Unicode kerning problem, into a separate ticket from the bounding box problem?

P.S.: I didn't have time yet to test CHTML and/or v4.

[dpvc]

Would it be adviseable to split off the Unicode kerning problem, into a separate ticket from the bounding box problem?

Not at this point. That is already resolved in v4. Once that is released, we will look into back-porting some bug fixes like this, but there is not need to make a new issue at this point.

[Jean-Luc-Picard-2021]

I tried CHTML v3. It shows an error message as soon as I use non-Latin. Characters, for example the greek λ and μ. So I cannot test CHTML and the Unicode Kerning problem.

This is CHTML without Greek, replaced it by ASCII \ and /:

This is CHTML with Greek:

On the other hand SVG shows the Greek:

[dpvc]

OK, here's what's happening. The buss proofs macros need to figure out the size of the various pieces so that they can be properly placed, and that means they have to call the output renderer to ask it to determine how big they are. That is done by a MathItem that contains the expression to be measured and asking the output renderer to get its bounding box. The Mathitem also contains information about where the expression is within the document's DOM, but in this case, it is not hooked into the DOM, so those pointers are null. When the renderer tries to get the bounding box, it adds up all the bounding boxes for the characters in the expression and returns that, but if a character is not in its fonts, it tries to measure the width by putting it into a DOM element and measuring the width of that. That DOM element is supposed to be put into the same container as the expression itself, so that it has the same CSS affecting it, but in the case of this detached MathItem, there is not parent DOM item, and that causes the error message you are seeing (about the parent being null).

There are several possible work-arounds. One is to use

MathJax = {
  startup: {
    ready() {
      MathJax.startup.defaultReady();
      const jax = MathJax.startup.document.outputJax;
      Object.assign(jax, {
        _measureTextNode_: jax.measureTextNode,
        measureTextNode: function (textNode) {
          return (!this.math.start.node ? {w: .67, h: .75, d: .2} : this._measureTextNode_(node))
        }
      });
    }
  }
};

This checks if the MathItem has a DOM node and if not, it returns a generic bounding box (so just an approximation), otherwise it does its usual measuring. This will prevent the error, but may not get the spacing exactly right.

The other approach is to make sure that you only use characters that are in the MathJax fonts. In v4, the character coverage is much greater, but in v3, there are no upright Greek lower-case letters like the ones you are using, and that does trigger the problem described above. But you could use something like

\RightLabel{Ax}\UnaryInfC{$\phi$ ⊢ $\phi$}

to get the italic phi character that MathJax has. Or even

\RightLabel{Ax}\UnaryInfC{$\phi \vdash \phi$}

Of course, if you already have a lot of content, it might not be easy to change them. In that case, you could use

MathJax = {
  startup: {
    ready() {
      MathJax.startup.defaultReady();
      document.getElementById('render').disabled = false;
      MathJax.startup.document.inputJax[0].preFilters.add(({math}) => {
        math.math = math.math
                     .replace(/\u03C6/g, '$\\phi$')   // or \varphi if that is better
                     .replace(/\u03C7/g, '$\\chi$')
                     .replace(/\u03C8/g, '$\\psi$');
      });
    }
  }
};

in order have the Unicode characters mapped to the corresponding TeX macros in math mode. You could add other replacements as needed. For example, you could map x1 to $x_1$ or $\mathrm{x}_1$, if you like. But if you are using these characters in other expressions on your page, you might have to be more careful about the replacements, as these are being applied to every expression on the page. In that case, it might be best search for \begin{prooftree}...\end{prooftree} and then do the replacement on its contents. Let me know if you need that instead.

With this configuration, your example from your second post above (the only one I had the source for) would produce

[dpvc]

The original issue of the bounding box for the proof being incorrect is resolved in the pull request linked above.

[Jean-Luc-Picard-2021]

Sounds good! Will do some testing soon...

[dpvc]

The fix has been merged into the develop branch.

[Jean-Luc-Picard-2021]

Is the develop v4 branch different from the v3? In terms of the API to use MathJax? Somehow I cannot test it. With the test case as documented at the beginning of this issue.

I only changed the end of the HTML document to this here:

<script type="text/javascript" id="MathJax-script" async
        src="https://cdn.jsdelivr.net/npm/mathjax@4.0.0-beta.6/tex-chtml.js">
</script>

The rest is the samel, in that Math.typeset() is called after the output was generated. I then get this error:

Error: MathJax retry
    at Object.Mn [as retryAfter] (tex-chtml.js:1:125320)
    at Dn.enrich (tex-chtml.js:1:864349)
    at t.enrich (tex-chtml.js:1:866205)
    at Object.renderDoc (tex-chtml.js:1:114661)
    at pn.renderDoc (tex-chtml.js:1:114773)
    at t.render (tex-chtml.js:1:116221)
    at Ei.typeset (tex-chtml.js:1:33587)
    at HTMLButtonElement.main_async (package.html?_ijt=o229alrkvl53hc6r7d53l241nr&_ij_reload=RELOAD_ON_SAVE:78:25)

And output is not rendered:

[dpvc]

The retry error is part of MathJax's internal mechanism for handling dynamically loaded code. When you see this error, it means you need to be using the promise-based calls in order to handle the asynchronous loading of some piece of MathJax code. Since you are using MathJax.typeset(), which is the synchronous call that doesn't handle dynamic code, you need to switch to MathJax.typesetPromise() and deal with the promises that allow the handling of asynchronous loading of code.

The reason you are getting that in v4 but didn't in v3 is because v4 introduced new fonts that have much larger glyph coverage, and the font data is now broken into multiple smaller pieces to reduce the initial download and only loads some character data as it is needed. That means the output rendering can be asynchronous where it wasn't in v3. See the release notes for the alpha release for more details.

You should be able to use the new bussproofs extension with v3 (though you will get a console warning about version mismatches).