Zulip Chat Archive

Stream: new members

Topic: doc-gen for a non-mathlib project


view this post on Zulip Julian Berman (Sep 28 2020 at 00:48):

I managed to make something (horrid, ugly and cargo culted) but functioning this afternoon

view this post on Zulip Julian Berman (Sep 28 2020 at 00:49):

The Sphinx part is here: https://github.com/Julian/sphinxcontrib-lean/

view this post on Zulip Julian Berman (Sep 28 2020 at 00:49):

Though I didn't add the auto-generator (using export_json.lean) fully yet

view this post on Zulip Julian Berman (Sep 28 2020 at 00:49):

But it does function (again, uglily). Sample output is... https://lean-across-the-board.readthedocs.io/en/sphinxed/ which is generated by the docs in this lean project: https://github.com/Julian/lean-across-the-board/tree/sphinxed/docs

view this post on Zulip Julian Berman (Sep 28 2020 at 00:50):

Not sure if that's interesting to other folks at all, if not was a fun distraction for a bit. I'll likely keep poking at it mostly to make the generator work a bit better (it's all just cobbling together code from other Sphinx domains essentially). but first will try and refocus on Lean itself for a few days.


Last updated: May 15 2021 at 02:11 UTC