feat: use docgen-action for documentation generation

[jessealama]

Uses leanprover-community/docgen-action to build & deploy docs.

Closes #121

[chenson2018]

Adding @fmontesi as reviewer since he setup these docs.

[chenson2018]

I'm intentionally not approving the workflow to run yet so that this doesn't accidentally builds docs here, as this currently does so for PRs.

[fmontesi]

Where does this publish the docs, exactly?

[chenson2018]

I think it targets the repo's GitHub pages by default, so something like leanprover.github.io/cslib

[fmontesi]

@leodemoura @kim-em (CC @swaratchaudhuri @barrettcw): Could we somehow set this up to write to https://lean-lang.org/cslib/doc/api (in the spirit of https://lean-lang.org/doc/api)?

[jessealama]

I think it targets the repo's GitHub pages by default, so something like leanprover.github.io/cslib

Right, the idea was to take inspiration from Mathlib and publish the documentation to https://leanprover.github.io/cslib/docs using GitHub Pages, so we'd need to set that up. A somewhat more complex alternative would be to set up a separate docs repo like mathlib4_docs.

[fmontesi]

We do have that for now, that's where the doc is currently produced. Check out the code at https://github.com/cs-lean/cs-lean.github.io. It outputs to https://cs-lean.github.io/

[jessealama]

@leodemoura @kim-em (CC @swaratchaudhuri @barrettcw): Could we somehow set this up to write to lean-lang.org/cslib/doc/api (in the spirit of lean-lang.org/doc/api)?

Shall we make a separate issue for this?

[arademaker]

Let me work on that with @kim-em since it would be nice to have the website and the API working in sync.

[chenson2018]

@arademaker Just making sure you have seen this Zulip thread: https://leanprover.zulipchat.com/#narrow/channel/513188-CSLib/topic/documentation.20best.20practices/with/553824087

As @fmontesi and I agree there, it is desirable for all building of docs to happen in this repo. What I suggest is, exactly as is already done for Mathlib on the website, that we host the docs in this repo's GitHub pages and simply link to them.

We merge this PR, check that it is building the docs, and update the website to link here. No extra coordination is needed and we can do this now. (Which would be nice, because I believe that currently the docs appear nowhere..)

[arademaker]

To make clear, as I wrote here, I agree to accept this PR. But first, we need to ask Lean Fro to add an exception to the rule that redirects all addresses under leanprover.github.io to lean-lang.org. Otherwise, the documentation will not be accessible.

[chenson2018]

To make clear, as I wrote here, I agree to accept this PR. But first, we need to ask Lean Fro to add an exception to the rule that redirects all addresses under leanprover.github.io to lean-lang.org. Otherwise, the documentation will not be accessible.

Thanks for the detailed reply! I didn't realize about the redirect rule, but it seems otherwise we're on the same page.

[arademaker]

Hi @fmontesi, I am ok to merge this PR. I talked with @nomeata and he believes the directs from leanprover.github.io to lean-lang.org will not block the leanprover.github.io/cslib/docs, let us see. If that works, it would be the easier/safer solution for the docs/API.

[chenson2018]

I noticed here that there is a check for if the docs directory already exists. Do we need to go ahead and remove it in this PR for it to run properly?

[arademaker]

I noticed that too, but this did not cause any trouble to the action, right? I am thinking if we would like to eventually have the folder in the repo to test/debug document generation locally. We can rename it to docbuild to avoid any confusion too.

[chenson2018]

I noticed that too, but this did not cause any trouble to the action, right? I am thinking if we would like to eventually have the folder in the repo to test/debug document generation locally. We can rename it to docbuild to avoid any confusion too.

I think it stops building when it sees the directory, because that step only ran for one second and there is none of the output I would expect from the docs building.

[arademaker]

Indeed, analysing it more carefully, I dont see the artifact here as I see here.

[chenson2018]

With that confirmed, my preference is to remove the docs directory. My reasoning for this as opposed to renaming is that I don't think it is worth maintaining the separate manifest and toolchain for the relatively rare need to build docs locally. In the situations where that is required, it is simple enough to do so by adding the required docs lakefile yourself.

[arademaker]

There is a bib file in the docs that I can move to the website. I still don't have write permission in the repo, please go ahead and delete the folder.

[chenson2018]

Good catch on the references.bib file. This should stay in the repo as it is used when generating the docs. I couldn't find how to specify this to the action, so I asked on Zulip. If it's not supported currently I can make a (separate) PR for that.

For now I've removed the docs directory and moved references.bib to the root of the repo.

[arademaker]

This should stay in the repo as it is used when generating the docs.

I didn't know that. Maybe having it in "docbuild" is the solution? Let us see what people will say.

[chenson2018]

This should stay in the repo as it is used when generating the docs.

I didn't know that. Maybe having it in "docbuild" is the solution? Let us see what people will say.

Hmm, maybe. In the meantime I wouldn't consider this blocking, it just affects the rendering of a few links that we can follow up on. Is there anything else pending for this PR?