Skip to content

Conversation

@kim-em
Copy link
Contributor

@kim-em kim-em commented Jan 28, 2026

Fixes the "no such file or directory" error when building documentation with lake build FooLib:docs.

The library_facet docs includes references.bib in its staticFiles array and attempts to compute its trace via computeTrace. However, this file is only created by the bibPrepass target.

Without an explicit dependency on bibPrepass, Lake may attempt to compute the trace of references.bib before it exists, causing builds to fail with:

error: no such file or directory (error code: 2)
 file: /path/to/.lake/build/doc/references.bib

This PR adds the missing bibPrepass dependency to library_facet docs, matching the pattern already used in module_facet docs and coreTarget.

🤖 Prepared with Claude Code

The `library_facet docs` includes `references.bib` in its staticFiles
array and attempts to compute its trace via `computeTrace`. However,
this file is only created by the `bibPrepass` target, which runs
before module documentation is generated.

Without an explicit dependency on `bibPrepass`, Lake may attempt to
compute the trace of `references.bib` before it exists, causing
the build to fail with "no such file or directory" errors.

This fix adds the missing `bibPrepass` dependency, matching the
pattern already used in `module_facet docs` and `coreTarget`.

Fixes leanprover-community/docgen-action#18 (the underlying cause)
@hargoniX hargoniX merged commit 4dbbb80 into leanprover:main Jan 28, 2026
1 check passed
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

Successfully merging this pull request may close these issues.

[BUG] Cache key should be updated when references changes

2 participants