fix: fixes the doc generation

[arademaker]

This PR fixes the doc generation that was not working since Oct 14th (see https://github.com/cs-lean/cs-lean.github.io/actions?page=2)

[chenson2018]

I don't understand these changes to the docs manifest, can you explain?

[arademaker]

I am trying to understand what happened.

[arademaker]

Hi @chenson2018, I fixed the docs/lakefile.toml, so we can now run the doc generation locally. Previously, running lake build Cslib:docs was overwriting files in the same folder.

[arademaker]

Once this PR is accepted, I can move to #128

[chenson2018]

This seems like a more reasonable diff of the manifest, thanks! I think what happened is that during the last version bump that this was not updated properly and somehow got nightly-testing mixed in too. (Though this is not the original reason the docs stopped building, which was due to inactivity in the other repo that now has the website).

Is your plan to merge this, then add back these lines in the other repo? This is precisely the scenario that I mention in my latest comment on #128 that we would like to avoid. Having builds happening in two repos is undesirable. Imagine for instance the build fails (in either repo) for some reason, possibly external to the code. You now have two locations to debug and sync.

I maintain that we should go ahead with #128, which moves us to a more standard workflow and supersedes this directory completely, then just link to the website to the docs that are build here, exactly as we already do for Mathlib.

Tagging @fmontesi

[chenson2018]

Once this PR is accepted, I can move to #128

Ah I missed this before I began my comment, sorry. This PR becomes not strictly necessary after that, but I see no harm in fixing this anyway.

[arademaker]

Hi @chenson2018

This seems like a more reasonable diff of the manifest, thanks! I think what happened is that during the last version bump that this was not updated properly and somehow got nightly-testing mixed in too. (Though this is not the original reason the docs stopped building, which was due to inactivity in the other repo that now has the website).

The problem with my second-to-last commit was that in docs/lakefile.toml we had buildDir = ".", which caused doc-gen4 to generate its output directly inside docs, overwriting the lake-manifest.json. I guess @fmontesi never thought about generating the docs locally, so this problem never happened before.

But indeed, after spending some time today experimenting with leanprover/doc-gen4 and leanprover-community/docgen-action, I now understand your point — we really don’t need this directory in the repository, the docgen-action creates this folder in the VM during its execution (although I still don’t quite understand where the files actually end up!).

The previous error (from Oct 14th) in the doc generation was not due to inactivity in the cs-lean.github.io repo, see here.

Is your plan to merge this, then add back these lines in the other repo? This is precisely the scenario that I mention in my latest comment on #128 that we would like to avoid. Having builds happening in two repos is undesirable. Imagine for instance the build fails (in either repo) for some reason, possibly external to the code. You now have two locations to debug and sync.

I see your point; having an action in the cs-lean/cs-lean.github.io repo to build the docs isn't really a good idea —it makes one repo depend on the other. I agree that it would be best to trigger the doc generation in leanprover/cslib.

I maintain that we should go ahead with #128, which moves us to a more standard workflow and supersedes this directory completely, then just link to the website to the docs that are build here, exactly as we already do for Mathlib.

I am talking with the Lean FRO team about the URL redirects. Today, anything under leanprover.github.io is redirected to lean-lang.org. We will need to add an exception so leanprover.github.io/cslib/docs are not redirected. I guess this was the reason @fmontesi created the cs-lean/cs-lean.github.io repo.

For the website, we also have some options. We can have it together with the leanprover/cslib repo or in a separate repo as it is now. But this is another discussion.