Skip to content

fix: regenerate the HTML of the project after a cache hit #38

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.

Sign up for GitHub

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

Already on GitHub? Sign in to your account

Open
marcelolynch wants to merge 2 commits into
base: main
Choose a base branch
from
Open

fix: regenerate the HTML of the project after a cache hit #38

Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
70fed48
fix: regenerate the HTML of the project after a cache hit
marcelolynch Sep 16, 2026
f76f99b
docs: shorten the comment on the deletion of the HTML markers
marcelolynch Oct 1, 2026
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
9 changes: 9 additions & 0 deletions scripts/build_docs.sh
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -88,6 +88,15 @@ fi
# Disable an error message due to a non-blocking bug. See Zulip
MATHLIB_NO_CACHE_ON_UPDATE=1 ~/.elan/bin/lake update $NAME

# Delete the markers of the HTML pass of `doc-gen4`, so that the pass runs on
# each build. The `:docs` facet writes a marker `<target>.docs_built` in
# `.lake/build/doc-data/`, and Lake skips the pass while the marker is up to
# date. The cache restores the markers but not the HTML of the project.
# Before leanprover/doc-gen4#418, a marker also stays up to date after a change
# to a Lean file. The pass reads the cached database and takes about one minute
# for 3000 modules.
rm -f .lake/build/doc-data/*.docs_built

# Build the docs
~/.elan/bin/lake build $DOCS_FACETS

Expand Down