Documentation as a DSL - David Thrane Christiansen

Stream: Lean Together 2024

[Heather Macbeth]

Exciting talk!

Does the system support omitting some of the code from the document? This capability was missing in Alectryon, and I missed it.

[Max Nowak 🐉]

Wow this looks amazing and very promising, I am excited!

Q1: Will you be able to define custom “pretty math printers”, that will output LaTeX/Typst, with actual big operators etc? Will those be based on Syntax or Expr?

Q2: Will the infoview benefit from that, and be able to show pretty math instead?

[Julian Berman]

Perhaps an offbeat question - I think it's not very controversial to say that Sphinx would be a lot better than it is if it were not developed by essentially one person -- not because that person isn't amazing (he is) but it's simply too large, complex and complicated thing to develop, which is made worse because reviewing PRs is lots of work too, and even worse because Sphinx is ironically extremely underdocumented when it comes to things like extension). Do you see the need to proactively counteract that happening here, even though we're much smaller?

[David Thrane Christiansen]

@Heather Macbeth The code sample feature is an ordinary library that any user can implement themselves or change - in this respect it's unlike Alectryon. My implementation does have this feature, and it also allows a single document to contain multiple independent Lean environments

[Eric Wieser]

Looking forward to playing around with this!

In the slides you mention that good IDE support is one of the goals; but what about support in bad text editors / viewers, like say GitHub? Right now the lean syntax highlighter isn't very happy with https://github.com/leanprover/verso/blob/main/doc/UsersGuide/Basic.lean; have there been any discussion about separate file extensions for verso documents to avoid these situations, maybe .verso.lean?

[David Thrane Christiansen]

@Max Nowak 🐉 If you can write it in Lean, then you can write it here. The full power of Lean metaprogramming is available while elaborating a document into the Verso AST, and the full power of ordinary Lean programming is available at output generation time

[Julian Berman]

Oh, and one more question which I may have missed given I missed the beginning unfortunately -- what's the ReadTheDocs equivalent :) -- is there a broader plan for how downstream projects can host their docs, or essentially do things end with HTML generation and then presumably stuff uses GitHub pages or whatever fits their fancy?

[David Thrane Christiansen]

Max Nowak 🐉 said:

Q2: Will the infoview benefit from that, and be able to show pretty math instead?

I don't know about that part - I suspect not, but perhaps if it shows docs.

[David Thrane Christiansen]

@Julian Berman This is a good question! I've written a number of Sphinx extensions myself, and it's not always easy to figure out how to do it. I think your question has two aspects: how do we keep code quality high? and how do we spread out the knowledge of how to maintain it?

For the quality side, the current state of the project definitely reveals that I wrote it quickly in a couple of months. The plan is to pay back this debt now that there's a working, testable system, and I'd like to enable lots of automated linters and checks and the like. It definitely needs docstrings!

For spreading knowledge, I think we're in the same boat as Lean as a whole. The internals are a lot like the Lean elaborator, which helps with familiarity, but at the end of the day, it's just tough. As things settle down, external contributions will be more useful, and I also hope that the smaller core with genres living externally will result in a much smaller system than all of Sphinx.

[David Thrane Christiansen]

@Eric Wieser I don't have a specific plan for this, but it is something that will require more thought in general as we get more DSLs that are essentially "total conversion mods" of Lean. A file extension makes sense for sure.

[Eric Wieser]

I suppose in the shorter term, the highlighter can just give up on the rest of the document when it sees #lang, assuming verso documents will contain that

[David Thrane Christiansen]

@Julian Berman RE ReadTheDocs - there are not presently clear plans for this, but I'm hoping that this will be part of the Reservoir integration, at least for the software documentation genres. But I don't want to make promises before everything has settled down, and I don't think we should host random blogs.

[Eric Wieser]

I think ReadTheDocs found a niche before github pages allowed deploying HTML from arbitrary build processes; so perhaps such a hosting tool is no longer necessary

[David Thrane Christiansen]

We'll have to see - things like hyperlinks between docs may work more reliably with a standard hosting setup, but this is something to explore further

[Julian Berman]

I'm slightly less sure it's unnecessary -- I think RTD is still super great and takes away needing to know much about how to set up CI -- but I agree it's a lot less hard than it used to be, and that uses: someaction/build-my-docs + the GH Pages action may be good enough.

[Julian Berman]

S... yeah. Intersphinx is amazing and the #1 thing I miss whenever I use any other system.

[David Thrane Christiansen]

Interverso is absolutely on the June roadmap

[Julian Berman]

Also doctesting. I hope there's some plan for that too?

[David Thrane Christiansen]

You can build doctests yourself as a library

[David Thrane Christiansen]

But something like them was already in today's demo, so it would be a small amount of work to adapt it

[Eric Wieser]

I guess one thing you can't get without read the docs is that .rtfd.io domain name...

[David Thrane Christiansen]

Including the code action to update them if they get out of date!

[Julian Berman]

Eric Wieser said:

I guess one thing you can't get without read the docs is that .rtfd.io domain name...

(and another -- easy redirect support for when you move pages)

[David Thrane Christiansen]

Local docs are also important - not everyone is always on the Internet, so I want to have an easy way to grab the docs for the code I have on disk (like raco doc)

[Patrick Massot]

Max Nowak 🐉 said:

Wow this looks amazing and very promising, I am excited!

Q1: Will you be able to define custom “pretty math printers”, that will output LaTeX/Typst, with actual big operators etc? Will those be based on Syntax or Expr?

Q2: Will the infoview benefit from that, and be able to show pretty math instead?

This is mostly orthogonal to David's work. You will be able to plug in https://github.com/kmill/LeanTeX because you'll be able to plug in any Lean library.

[David Thrane Christiansen]

This is a good way to do it - math rendering in the editor need not be tied to a big documentation authoring framework - better to have a small, reusable library that works in both contexts