Zulip Chat Archive

Stream: general

Topic: Running doc-gen on /archive


Eric Wieser (Feb 01 2021 at 17:01):

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 (Feb 01 2021 at 17:02):

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 (Feb 01 2021 at 17:03):

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

Eric Wieser (Feb 01 2021 at 17:07):

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 (Feb 01 2021 at 17:14):

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 (Feb 01 2021 at 17:16):

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 (Feb 01 2021 at 17:18):

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 (Feb 01 2021 at 17:23):

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 (Feb 01 2021 at 17:23):

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


Last updated: Dec 20 2023 at 11:08 UTC