Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Building HTML documentation instructions fails on clean clone #15369

Open
oeb25 opened this issue Jul 31, 2024 · 1 comment
Open

Building HTML documentation instructions fails on clean clone #15369

oeb25 opened this issue Jul 31, 2024 · 1 comment

Comments

@oeb25
Copy link
Collaborator

oeb25 commented Jul 31, 2024

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)
@oeb25
Copy link
Collaborator Author

oeb25 commented Jul 31, 2024

This might be related to leanprover-community/batteries#669 but the current docs already has the -R flag, so I'm not quite sure.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

No branches or pull requests

1 participant