fix: regenerate the HTML of the project after a cache hit - #38
Open
marcelolynch wants to merge 2 commits into
Open
marcelolynch wants to merge 2 commits into
marcelolynch wants to merge 2 commits into
Conversation
marcelolynch
force-pushed
the
fix/regenerate-project-html-on-cache-hit
branch
from
September 16, 2026 18:57
fe89d05 to
a49fae0
Compare
The `:docs` facet of `doc-gen4` gates its HTML pass on an empty marker `<target>.docs_built` in `.lake/build/doc-data/`. Lake runs the pass when the marker is absent or when the hash of its dependency trace differs from the saved hash. The HTML files are outside this check. The trace changes only with the `doc-gen4` executable and the bibliography. The `docInfo` markers which feed it are empty files, and Lake takes the trace of a built file from its content, so the hash of each marker is constant. The cache holds the markers, because it holds `doc-data`. It holds the HTML of the dependencies only, because the cached paths come from the packages in `lake-manifest.json`, and the project is not one of them. After a cache hit, Lake therefore skips the pass on every push, and the site has no pages for the project. Each page of the project gives a 404. This commit deletes the markers after the cache restore. The pass then runs on each build and writes the HTML from the cached database. It takes about one minute for a project with 3000 modules in its import closure. This ports dwrensha/docgen-action@8c6b36d by David Renshaw. Fixes leanprover-community#33 Refs leanprover-community#28 Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com>
marcelolynch
force-pushed
the
fix/regenerate-project-html-on-cache-hit
branch
from
September 16, 2026 19:22
a49fae0 to
70fed48
Compare
This was referenced Sep 16, 2026
marcelolynch
marked this pull request as ready for review
September 25, 2026 20:15
The comment now also holds for doc-gen4 versions that include leanprover/doc-gen4#418. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Fixes #33. Refs #28.
This ports dwrensha/docgen-action@8c6b36d by @dwrensha.
After a cache hit, each page of the project can give a 404. The
:docsfacet ofdoc-gen4writes the HTML in one pass and records the pass in a marker<target>.docs_builtin.lake/build/doc-data/(seegenerateHtmlDocs). Lake checks the marker, not the HTML. The cache restores the marker but not the HTML of the project, so Lake skips the pass and the project has no pages. A cache miss gives a fresh build, so the bug looks intermittent. In doc-gen4 versions before leanprover/doc-gen4#418, the marker also stays up to date after a change to a Lean file.This PR deletes the markers before
lake build, so the HTML pass runs on each build. The cache paths and the key do not change. The pass reads the cached database. In a Noperthedron run with 2936 modules, it took 71 s.To test: a run on
mainafter a cache hit and a change to a Lean file has no pages for the project. The same run on this branch has all pages.🤖 Generated with Claude Code