Skip to content

fix: lake: report a missing library root file - #14625

Merged
tydeu merged 5 commits into
leanprover:masterfrom
jcreinhold:lake-missing-lib-root-error
Aug 2, 2026
Merged

fix: lake: report a missing library root file#14625
tydeu merged 5 commits into
leanprover:masterfrom
jcreinhold:lake-missing-lib-root-error

Conversation

@jcreinhold

@jcreinhold jcreinhold commented Jul 31, 2026 •
edited
Loading

Copy link
Copy Markdown
Contributor

This PR makes Lake report the underlying file error when a lean_lib root module has no source file, instead of only reporting that some modules have bad imports.

LeanLib.recCollectLocalModules now retains failed modules reached directly from getModuleArray so their build jobs expose the error, while continuing to omit failures reached through imports because their importers report them.

Closes #14619

@jcreinhold
fix: lake: report a missing library root file
c12a117 
This PR makes Lake report the real error when a `lean_lib` root module has no source file. Building `lean_lib A` with only `A/One.lean` and no `A.lean` reported `A: some modules have bad imports` and discarded the real error, `no such file or directory: A.lean`.

`LeanLib.recCollectLocalModules` dropped the module from the library's module set, so Lake never built it and never reported its error. The comment there says the error surfaces later when the module is built. That holds for a module reached through an import, which `collectImportsAux` reports against the importer, but not for one from `getModuleArray`, which has no importer. Lake now keeps such modules and still drops imported ones, so no second error appears where the importer already reports one.

Closes leanprover#14619
@jcreinhold
jcreinhold force-pushed the lake-missing-lib-root-error branch from ac83cb5 to c12a117 Compare July 31, 2026 21:18
@jcreinhold

jcreinhold commented Jul 31, 2026 •
edited
Loading

Copy link
Copy Markdown
Contributor Author

Two calls I'm not sure about:

Summary line. A: some modules have bad imports still prints above the real error. Reword it? Costs an update to tests/lake/tests/badImport/test.sh:15.

Location. #14619 points 1–2 suggest Glob.forEachModuleIn instead. I avoided it: that glob also serves lean_exe roots and governs files that vanish mid-build, which badImport tests.

Note: a declared module with no source now sits in the module set, so lake query lib:modules lists it.

@github-actions github-actions Bot added the toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN label Jul 31, 2026
@mathlib-lean-pr-testing

mathlib-lean-pr-testing Bot commented Jul 31, 2026

Copy link
Copy Markdown

Mathlib CI status (docs):

  • ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 23393b959b33e3a8d15796b2397f8a04c315b9f4 --onto 5b8d06c1764fa367a1e27b3e89f64667eac425af. You can force Mathlib CI using the force-mathlib-ci label. (2026-07-31 21:43:16)

@leanprover-bot

leanprover-bot commented Jul 31, 2026 •
edited
Loading

Copy link
Copy Markdown
Collaborator

Reference manual CI status:

  • ❗ Reference manual CI will not be attempted unless your PR branches off the nightly-with-manual branch. Try git rebase 23393b959b33e3a8d15796b2397f8a04c315b9f4 --onto a39eab69e1eee9ad38f4efe507907b1026a77808. You can force reference manual CI using the force-manual-ci label. (2026-07-31 21:43:17)
  • ❗ Reference manual CI can not be attempted yet, as the nightly-testing-2026-08-02 tag does not exist there yet. We will retry when you push more commits. If you rebase your branch onto nightly-with-manual, reference manual CI should run now. You can force reference manual CI using the force-manual-ci label. (2026-08-02 15:35:51)

tydeu
tydeu reviewed Aug 1, 2026
View reviewed changes

@tydeu tydeu left a comment

Copy link
Copy Markdown
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

This looks good overall! However, the error message in recCollectLocalModules needs to be updated to cover both cases. I think it should be kept, as it serves as a good summary when there are multiple errors with roots.

I am not sure what the best message would be. Maybe something like "some modules have bad imports or could not be found". Feel free to suggest something better!

@jcreinhold

jcreinhold commented Aug 2, 2026

Copy link
Copy Markdown
Contributor Author

@tydeu I added a "... could not be read" to the error message. I also changed the new variable name from declared to viaImport to try to make it a bit more obvious/clear. Happy to change either!

@jcreinhold
jcreinhold marked this pull request as ready for review August 2, 2026 14:45
@tydeu tydeu added the changelog-lake Lake label Aug 2, 2026
tydeu
tydeu approved these changes Aug 2, 2026
View reviewed changes

@tydeu tydeu left a comment

Copy link
Copy Markdown
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Thank you! 🎉 LGTM!

@tydeu
tydeu added this pull request to the merge queue Aug 2, 2026
Merged via the queue into leanprover:master with commit cdd822a Aug 2, 2026
27 of 29 checks passed
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@tydeu tydeu tydeu approved these changes

Assignees

No one assigned

Labels

changelog-lake Lake toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

lake: missing lean_lib root file reported as "some modules have bad imports"

3 participants

@jcreinhold @leanprover-bot @tydeu