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.toml
s - 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 example
s. 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