documentation best practices

Stream: CSLib

[Chris Henson]

In #mathlib4 > can't `lake update` @ 💬 it is suggested that the current best practice for documentation is to use leanprover-community/docgen-action. I'd like to do this for a few reasons:

• it standardizes the documentation build, which currently sets up and builds everything by hand
• it eliminates the current hassle of checking that the docs toolchain is synced, something people have to remember and a CI annoyance
• it puts the documentation workflow in a more standard place (it is currently in the old organization), preferably built on commits to main rather than on a cron basis

I can't think of any problems off the top of my head, am I missing any tradeoffs? There is a small point of figuring out where it will deploy to, that's all I could think of.

[Fabrizio Montesi]

Can we just patch this maybe? https://github.com/cs-lean/cs-lean.github.io/blob/main/.github/workflows/update-cslib-docs.yaml

[Chris Henson]

We can certainly make changes incrementally there, like making it use the action first. Long-term though, I think it would be best for it to be in our organization/repo.

[Fabrizio Montesi]

Ah, definitely. It's in the plans of the SG as well, but we gotta find a place. We'll probably look at this again after we finish a webpage for cslib

[Chris Henson]

@Fabrizio Montesi The documentation workflow is no longer running because GitHub by default disabled it after 60 days of inactivity in the old repo. You can probably make a trivial commit or retrigger manually for now, but I am partial to us getting cslib#128 merged.

[Chris Henson]

My preference would be to merge that, using the default location for GitHub pages which would now be tied to the leanprover/cslib repo, then figure out the domain you suggested later. We can have the old url (https://cs-lean.github.io/) redirect for compatibility, but it is better IMO to go ahead and do this now rather than have to keep one isolated workflow in an unaffiliated repo.

[Fabrizio Montesi]

Thanks for noticing, I was wondering why it wasn't updating yesterday! @Alexandre Rademaker is working on that repo to make a website for cslib, which will include the API documentation. It'll all be available at cs-lean.github.io for now, we'll then move it somewhere else in the future.

[Chris Henson]

No problem. I don't check the docs that often, it's actually been a couple of weeks...

I'm not sure I've conveyed well what I'm requesting above. I am asking that the documentation should be built, regardless of where it is deployed now or eventually to an external site, in a workflow that lives in leanprover/cslib. This preempts problems like this and generally simplifies CI, and this is something we can do now. Does that seem reasonable?

[Fabrizio Montesi]

You mean adding a check that docs can be built in our CI? If so, YES PLEASE! :-)

[Chris Henson]

I mean that they are built in our CI, and then distributed to wherever you would like.

[Fabrizio Montesi]

How would they be distributed?

[Fabrizio Montesi]

commit to a remote repo of the built doc files?

[Chris Henson]

GitHub pages even support custom domains, they could just live in leanprover/cslib's GitHub pages. If they really need to be sent somewhere else, there are actions to send artifacts.

[Chris Henson]

I just do not want to have documentation builds spread across different repos. It is a recipe for confusion.

[Fabrizio Montesi]

ah yes, sure. @Alexandre Rademaker let's look into this after we're done with v1 of the website. It is good to centralise where we build stuff from the cslib repo.

[Chris Henson]

Okay, thanks! Whatever short term fix is probably fine (if you make a commit in the old repo I guess that buys two months, though I still vote for trying cslib#128 as it won't hurt anything), and we'll just keep this in mind for later. Once upon a time I did DevOps work, it seems I have unwittingly found a use for that knowledge again...

[Chris Henson]

This has been merged and the first deployment was successful! Thanks again to @Jesse Alama for taking up this PR. It is great to have folks proactively make and address GitHub issues.

The docs now appear at https://leanprover.github.io/cslib/docs/. @Alexandre Rademaker can you update the website to use this link?