Zulip Chat Archive

Stream: general

Topic: doc-gen on windows

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?

Kevin Buzzard (Feb 11 2021 at 08:51):

C'est trop con.

Sebastien Gouezel (Feb 11 2021 at 08:52):

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

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

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

Sebastien Gouezel (Feb 11 2021 at 09:16):

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

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

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

Eric Wieser (Feb 11 2021 at 09:17):

Replace align* with align?

Eric Wieser (Feb 11 2021 at 09:19):

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

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.

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.

Eric Wieser (Feb 11 2021 at 11:14):

I think this is a quirk in the markdown parser

Last updated: Dec 20 2023 at 11:08 UTC