Zulip Chat Archive

Stream: lean4

Topic: Building lean4_docs like mathlib4_docs


Siddharth Bhat (Feb 15 2022 at 11:41):

I spun up a small repo to generate lean4 docs with doc-gen4, bollu.github.io/lean4_docs [The github repo is https://github.com/bollu/lean4_docs]. I feel it'd be useful for it to be under leanprover/lean4_docs`, since we can then write a deploy script that updates the latest version of the docs. What do others feel?

Mac (Feb 26 2022 at 22:33):

I think this sounds like a good idea. Maybe it could somehow be combine with @Xubai Wang's Reservoir package index?


Last updated: Dec 20 2023 at 11:08 UTC