Zulip Chat Archive

Stream: general

Topic: doc-gen on windows


view this post on Zulip Sebastien Gouezel (Feb 11 2021 at 08:50):

Did you know it is not possible (or rather, I wasn't able) to run doc-gen on windows because of docs#con and the fact that you can't create a directory named con?

view this post on Zulip Kevin Buzzard (Feb 11 2021 at 08:51):

C'est trop con.

view this post on Zulip Sebastien Gouezel (Feb 11 2021 at 08:52):

I thought only French people could get the additional joke :-)

view this post on Zulip Sebastien Gouezel (Feb 11 2021 at 09:08):

I wanted to experiment on my computer to understand why mathjax doesn't like the latex block just before docs#formal_multilinear_series.radius_right_inv_pos_of_radius_pos_aux1, while it looks good in https://observablehq.com/@bryangingechen/github-lean-doc-preview?url=%22https%3A%2F%2Fgithub.com%2Fleanprover-community%2Fmathlib%2Fblob%2Fmaster%2Fsrc%2Fanalysis%2Fanalytic%2Finverse.lean%22#docs

I wonder if it is due to the \\&, which latex parses as: go to next line, and then insert the spacing character & for the align block, but that the mathjax seems to parse in a different order, as: use the second backslash to escape the &, and then be confused by the remaining first backslash. I have pushed a branch mathjax with this change, but I don't know if I have a way to check the resulting documentation without building it locally (and I won't PR it to mathlib if I don't know whether it fixes the issue...)

view this post on Zulip Eric Wieser (Feb 11 2021 at 09:12):

I thought I fixed this: https://github.com/leanprover-community/doc-gen/blob/91815a109b73629324adad72355f9c83c510e417/print_docs.py#L482

view this post on Zulip Sebastien Gouezel (Feb 11 2021 at 09:16):

Looks like the problem comes from doc-gen, not mathjax: the html source code is

<p>$$
\begin{align<em>}
Q(z) &amp; := \sum Q_n z^n = Q_1 z + C' \sum_{2 \leq k \leq n} \sum_{i_1 + \dotsc + i_k = n}
  (r z^{i_1} Q_{i_1}) \dotsm (r z^{i_k} Q_{i_k})
\&amp; = Q_1 z + C' \sum_{k = 2}^\infty (\sum_{i_1 \geq 1} r z^{i_1} Q_{i_1})
  \dotsm (\sum_{i_k \geq 1} r z^{i_k} Q_{i_k})
\&amp; = Q_1 z + C' \sum_{k = 2}^\infty (r Q(z))^k
= Q_1 z + C' (r Q(z))^2 / (1 - r Q(z)).
\end{align</em>}
$$</p>

so it is not surprising mathjax can't do anything out of it.

view this post on Zulip Eric Wieser (Feb 11 2021 at 09:17):

Replace align* with align?

view this post on Zulip Eric Wieser (Feb 11 2021 at 09:19):

Oh right, i missed the \\ issue you describe too

view this post on Zulip Sebastien Gouezel (Feb 11 2021 at 09:23):

Yes, changing align* to align may help also. Hopefully, the mathjax branch should work fine, but to check this I will need to understand why your fix to con files doesn't work on my computer.

view this post on Zulip Sebastien Gouezel (Feb 11 2021 at 11:03):

I could fix the build on my machine, see https://github.com/leanprover-community/doc-gen/pull/109.

Still, I can't get my latex block to show up as I want it to. Or rather, I can, but it means replacing \\ with \\\\ in the source so that it gets converted to \\ in the html file. But this is ugly in the source file. I'd much rather adapt the docs generation, but I can't tell where the translation to html takes place (the one that changes * to <em> in \begin{align*}, and \\& to \&amp;) so I can' try to tweak it.

view this post on Zulip Eric Wieser (Feb 11 2021 at 11:14):

I think this is a quirk in the markdown parser


Last updated: May 16 2021 at 20:13 UTC