You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
When cloning a fresh version of mathlib (9610549 specifially) and running the instructions for building the HTML documentation fails with:
❯ lake -R -Kdoc=on update doc-gen4
lake build Mathlib:docs
info: batteries: cloning https://github.com/leanprover-community/batteries to '././.lake/packages/batteries'
info: Qq: cloning https://github.com/leanprover-community/quote4 to '././.lake/packages/Qq'
info: aesop: cloning https://github.com/leanprover-community/aesop to '././.lake/packages/aesop'
info: proofwidgets: cloning https://github.com/leanprover-community/ProofWidgets4 to '././.lake/packages/proofwidgets'
info: importGraph: cloning https://github.com/leanprover-community/import-graph to '././.lake/packages/importGraph'
info: Cli: cloning https://github.com/leanprover/lean4-cli to '././.lake/packages/Cli'
info: mathlib: running post-update hooks
error: unknown library facet `docs`
System information:
❯ elan --version
elan 3.1.1 (71ddc6633 2024-02-22)
❯ lean --version
Lean (version 4.10.0, arm64-apple-darwin23.5.0, commit c375e19f6b65, Release)
❯ lake --version
Lake version 5.0.0-c375e19 (Lean version 4.10.0)
The text was updated successfully, but these errors were encountered:
When cloning a fresh version of mathlib (9610549 specifially) and running the instructions for building the HTML documentation fails with:
System information:
The text was updated successfully, but these errors were encountered: