doc-gen on windows

Stream: general

[Sebastien Gouezel]

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?

[Kevin Buzzard]

C'est trop con.

[Sebastien Gouezel]

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

[Sebastien Gouezel]

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...)

[Eric Wieser]

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

[Sebastien Gouezel]

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.

[Eric Wieser]

Replace align* with align?

[Eric Wieser]

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

[Sebastien Gouezel]

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.

[Sebastien Gouezel]

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 \&) so I can' try to tweak it.

[Eric Wieser]

I think this is a quirk in the markdown parser