editor for writing docstrings

Stream: general

[Kevin Buzzard]

So usually when I write a half-decent attempt at a module docstring, I have a go with the 's and the $$s and mixing unicode and TeX, but I occasionally get it wrong, and then when I make the PR Bryan comes along within an hour and tidies up all the typesetting errors I've made. How is Bryan doing this? Is there a way for me to take a local lean file and view the corresponding module docstring in a browser as it would be displayed in the API documentation (a module docstring documents an entire .lean file , right?) I would be a better module docstring writer if I knew how to do this.

In fact I probably think it's worth saying at this point how brilliant @Bryan Gin-ge Chen is. I've never even met him, but every PR I make he goes straight in there and fixes up little slips I've made like an incorrectly formatted commit name or a docstring markup mess -- he's training me to be a better PR maker and hence less trouble to the maintainers (he also taught me about correct use of tags).

[Eric Wieser]

The unpleasant answer is "just run doc-gen locally", but that takes forever to generate the export data and I don't actually recommend it.

[Sebastien Gouezel]

The pleasant answer is: use https://observablehq.com/@bryangingechen/github-lean-doc-preview (give a PR number, and it will show you the rendered docstrings)

[Johan Commelin]

we should have a zulip linkifier for this

[Johan Commelin]

something like docpreview#1234

[Rob Lewis]

I don't know if the preview accepts the PR number as part of the url, and in any case, Zulip's linkifier complains about the @ in the url. So for now, #docpreview one sec

[Rob Lewis]

#docpreview

[Johan Commelin]

thanks Rob!

[Bryan Gin-ge Chen]

Thanks Kevin! I'm glad the previewer is still useful. I haven't been advertising it much lately, but I do find it helpful previewing the output of docstrings and module docs. Note that there can be differences with what actually shows up in the final rendered docs, either due to weird parsing hacks I resorted to or due to markdown2 limitations on the doc-gen side.