doc-gen for a non-mathlib project

Stream: new members

[Julian Berman]

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

[Julian Berman]

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

[Julian Berman]

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

[Julian Berman]

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

[Julian Berman]

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.