Running doc-gen on /archive

Stream: general

[Eric Wieser]

In principle, we could have a new "archive" subheading in the sidebar to complement "core", and "mathlib". Is this a good idea?

[Bryan Gin-ge Chen]

I've wondered about this before too. I think want to have some kind of nice proof display though; just displaying the declarations and their types probably isn't too useful.

[Eric Wieser]

Well, it would at least show what has been proved in lean, and gives links back to the source

[Eric Wieser]

I thought about giving this a go myself, but I'm confused by the fact that archive has no leanpkg.toml

[Bryan Gin-ge Chen]

As far as CI goes we just use the one in the root of mathlib. As far as I can tell, if you tell Lean explicitly which directories to compile, then the path = "src" line in leanpkg.toml doesn't matter.

[Eric Wieser]

Ah, ok. doc-gen currently forms the subheadings by counting leanpkg.tomls - so I guess either CI needs to inject such a file at build time, or it needs another way to find them

[Bryan Gin-ge Chen]

While this is on my mind, there are a few archive/ proofs that are examples. Those should probably be changed, otherwise I think they won't show up.

[Eric Wieser]

Oh, a bigger problem is that doc-gen works by first importing everything, but the files in archive do not make any effort to be in a unique namespace

[Eric Wieser]

So things like problem_predicate are likely to clash between imo questions, for instance