bussproofs layout: overlapping text + too small SVG

[FliegendeWurst]

Issue Summary

The example below renders incorrectly (see screenshot). Two of the axioms are overlapping and the SVG width is set too low (->overflow).

Steps to Reproduce:

Render this (I used https://mathjax.github.io/MathJax-demos-web/input-tex2svg.html):

\begin{prooftree}
\AxiomC{$(\texttt{AAAAAAAAAAAA})(\texttt{x})=$}
\UnaryInfC{8}
\AxiomC{$(\texttt{AAAAAAAAAAAA})(\texttt{x})=$}
\UnaryInfC{7}
\BinaryInfC{6}
\UnaryInfC{5}
\AxiomC{$(\texttt{AAAAAAAAAAAA})(\texttt{h})=$}
\UnaryInfC{4}
\AxiomC{$(\texttt{AAAAAAAAAAAA})(\texttt{g})=$}
\UnaryInfC{3}
\BinaryInfC{2}
\UnaryInfC{1}
\BinaryInfC{last}
\end{prooftree}

Technical details:

• MathJax Version: 3.1.2
• Client OS: Linux (nixOS)
• Browser: Firefox 84

[Feuermagier]

Same problem here. I noticed that the overflow will only happen if the prooftree is growing to the right of the root. To the left MathJax will set the width correctly.

[zorkow]

Thanks for reporting these. There are indeed a couple of issues with layout, in particular when formulas or labels grow too large. Likewise, the sequent calculus style rules have some layout problems. Sometimes it helps to swap label site, but that often only mirrors the issue.
The fact is that bussproofs is still a bit experimental, as it becomes clear that a MathML-based rendering model entirely unsuitable for complex layout of that nature. I have it on the agenda for the 3.2 release to revamp the layout and rendering algorithm. So if you have other corner cases or real world examples with problems, please add them to this thread, as they would be helpful for development.

[FliegendeWurst]

Here is a real example: (type inference of a lambda term)

(click to expand)

``` \begin{prooftree} \AxiomC{$(\texttt{g}:\beta_{1},\texttt{x}:\alpha_{4},\texttt{y}:\alpha_{6})(\texttt{y})=\alpha_{6}$} \LeftLabel{VAR} \UnaryInfC{$\texttt{g}:\beta_{1},\texttt{x}:\alpha_{4},\texttt{y}:\alpha_{6}\vdash\texttt{y}:\alpha_{8}$} \AxiomC{$(\texttt{g}:\beta_{1},\texttt{x}:\alpha_{4},\texttt{y}:\alpha_{6})(\texttt{x})=\alpha_{4}$} \LeftLabel{VAR} \UnaryInfC{$\texttt{g}:\beta_{1},\texttt{x}:\alpha_{4},\texttt{y}:\alpha_{6}\vdash\texttt{x}:\alpha_{10}$} \AxiomC{$(\texttt{g}:\beta_{1},\texttt{x}:\alpha_{4},\texttt{y}:\alpha_{6})(\texttt{y})=\alpha_{6}$} \LeftLabel{VAR} \UnaryInfC{$\texttt{g}:\beta_{1},\texttt{x}:\alpha_{4},\texttt{y}:\alpha_{6}\vdash\texttt{y}:\alpha_{11}$} \LeftLabel{APP} \BinaryInfC{$\texttt{g}:\beta_{1},\texttt{x}:\alpha_{4},\texttt{y}:\alpha_{6}\vdash\texttt{x}\ \texttt{y}:\alpha_{9}$} \LeftLabel{APP} \BinaryInfC{$\texttt{g}:\beta_{1},\texttt{x}:\alpha_{4},\texttt{y}:\alpha_{6}\vdash\texttt{y}\ (\texttt{x}\ \texttt{y}):\alpha_{7}$} \LeftLabel{ABS} \UnaryInfC{$\texttt{g}:\beta_{1},\texttt{x}:\alpha_{4}\vdash\lambda \texttt{y}.\ \texttt{y}\ (\texttt{x}\ \texttt{y}):\alpha_{5}$} \LeftLabel{ABS} \UnaryInfC{$\texttt{g}:\beta_{1}\vdash\lambda \texttt{x}.\ \lambda \texttt{y}.\ \texttt{y}\ (\texttt{x}\ \texttt{y}):\alpha_{2}$} \AxiomC{$(\texttt{g}:\beta_{1},\texttt{z}:\alpha_{12},\texttt{a}:\alpha_{14})(\texttt{z})=\alpha_{12}$} \LeftLabel{VAR} \UnaryInfC{$\texttt{g}:\beta_{1},\texttt{z}:\alpha_{12},\texttt{a}:\alpha_{14}\vdash\texttt{z}:\alpha_{18}$} \AxiomC{$(\texttt{g}:\beta_{1},\texttt{z}:\alpha_{12},\texttt{a}:\alpha_{14})(\texttt{g})=\beta_{1}$} \LeftLabel{VAR} \UnaryInfC{$\texttt{g}:\beta_{1},\texttt{z}:\alpha_{12},\texttt{a}:\alpha_{14}\vdash\texttt{g}:\alpha_{19}$} \LeftLabel{APP} \BinaryInfC{$\texttt{g}:\beta_{1},\texttt{z}:\alpha_{12},\texttt{a}:\alpha_{14}\vdash\texttt{z}\ \texttt{g}:\alpha_{16}$} \AxiomC{$(\texttt{g}:\beta_{1},\texttt{z}:\alpha_{12},\texttt{a}:\alpha_{14})(\texttt{a})=\alpha_{14}$} \LeftLabel{VAR} \UnaryInfC{$\texttt{g}:\beta_{1},\texttt{z}:\alpha_{12},\texttt{a}:\alpha_{14}\vdash\texttt{a}:\alpha_{17}$} \LeftLabel{APP} \BinaryInfC{$\texttt{g}:\beta_{1},\texttt{z}:\alpha_{12},\texttt{a}:\alpha_{14}\vdash\texttt{z}\ \texttt{g}\ \texttt{a}:\alpha_{15}$} \LeftLabel{ABS} \UnaryInfC{$\texttt{g}:\beta_{1},\texttt{z}:\alpha_{12}\vdash\lambda \texttt{a}.\ \texttt{z}\ \texttt{g}\ \texttt{a}:\alpha_{13}$} \LeftLabel{ABS} \UnaryInfC{$\texttt{g}:\beta_{1}\vdash\lambda \texttt{z}.\ \lambda \texttt{a}.\ \texttt{z}\ \texttt{g}\ \texttt{a}:\alpha_{3}$} \LeftLabel{APP} \BinaryInfC{$\texttt{g}:\beta_{1}\vdash(\lambda \texttt{x}.\ \lambda \texttt{y}.\ \texttt{y}\ (\texttt{x}\ \texttt{y}))\ (\lambda \texttt{z}.\ \lambda \texttt{a}.\ \texttt{z}\ \texttt{g}\ \texttt{a}):\alpha_{1}$} \end{prooftree} ```