doc-gen4 for projects depending on mathlib

Stream: lean4

[Sky Wilshaw]

In lean 3, doc-gen would create documentation for all of the mathlib definitions and theorems that were used in a given project, and bundle them in the same documentation webpage as the project's own definitions and theorems. Is there a way I can replicate this behaviour with doc-gen4, or (even better) get mathlib links to redirect to mathlib's own documentation? Currently they just 404 because the pages aren't built.

[Sky Wilshaw]

(Context: https://leanprover-community.github.io/con-nf/doc/)

[Henrik Böving]

No doc-gen4 currently doesn't support interlinking to different documentation pages. You could make it generate documentation for mathlib in this pages rather easily by also passing it Mathlib:docs as a target though

[Sky Wilshaw]

I'll give that a shot and see what it looks like. Is the syntax just ~/.elan/bin/lake -Kenv=dev build <my project>:docs Mathlib:docs?

[Henrik Böving]

Yes

[Henrik Böving]

Note that you probably also want to build the std docs...and that depending on your computer this will take a while

[Sky Wilshaw]

Well, it'll be running on CI so that's not as much of an issue. I'll see how long it takes and see what works best for my use case.