Read each library's srcDir under the package's srcDir

[Deicyde]

Lake puts a library's sources at the package directory, then the package's srcDir, then the library's srcDir (Package.srcDir and LeanLib.srcDir in Lake's configuration). lean_libraries joined the library's srcDir onto the project root and ignored the package's, so a project that sets srcDir on the package got the wrong module mapping. With a lakefile.toml holding name = "proj", srcDir = "pkgsrc" and a [[lean_lib]] named Proj, Lake builds pkgsrc/Proj.lean as the module Proj, but module_of called it pkgsrc.Proj and path_of("Proj", ...) found no file. A lakefile.lean with package proj where srcDir := "pkgsrc" has the same problem, since lake translate-config writes that as a top-level srcDir. autoform skeleton, autoform work impact and autoform unused-hypotheses (added in #198, after this branch was cut) all read libraries through lean_libraries, so all three get the corrected mapping. On a built project with srcDir := "src", the issue shows extraction stopping at error: unknown target src.Skel.Main.

lean_libraries now reads the top-level srcDir (default .) once and joins each library's srcDir onto it. A package without library targets is still read as one library named after the package, but its sources now come from the package's srcDir instead of the project root. Nothing changes for projects that set srcDir only on the library, which includes the projects autoform project new creates and the bundled example.

Tests

• test_libraries_nest_under_the_package_source_directory writes a lakefile.toml with a package-level srcDir. It checks src_dir, module_of and path_of in two cases: a library with its own srcDir, whose sources are in pkgsrc/lib, and a package without library targets, whose sources are in pkgsrc.
• test_lakefile_lean_libraries_nest_under_the_package_source_directory covers the lakefile.lean path with the translation stubbed.
• test_package_source_directory_nests_libraries_through_lake_translate_config runs the real lake translate-config on package proj where srcDir := "pkgsrc" with lean_lib Proj. Like its neighbours, it skips when the fixture's Lean toolchain is missing, so the real-Lean CI job is where it runs.

The issue also asked for a real-Lean test through lakefile.toml. lean_libraries parses lakefile.toml itself without calling Lake, so such a test would run the same code as the unit test above. Lake's own nesting of a library srcDir under the package srcDir is already pinned by a real build in tests/test_lake_artifact_audit.py::test_real_toml_build_uses_target_src_dir_globs_and_import_closure. No build-and-extract test was added.

The three cases of the first two tests fail on main and pass with the change. The machine was over its load limit, so pytest did not run locally. Instead, a small script called the test functions directly, one at a time. With the change, all 18 cases in the project-layout section of tests/test_skeleton.py pass, the new ones included. Against main, the three new cases fail and the two existing source-directory tests pass. CI passed every check on a8b3e16, and its pull-request run tested the merge into an older main. In that run, the real-Lean job ran the skeleton suite with AUTOFORM_REQUIRE_REAL_LEAN_TESTS=1, which turns a missing toolchain into an error instead of a skip; 182 tests passed and none were skipped, so the translate-config test ran. Main has moved since; the change still merges cleanly, and nothing merged since touches lean_libraries or the files that call it. ruff check autoform_cli servers tests is clean.

Overlaps with open PRs

• Allow proof imports with measured impact #183 edits the same lines of lean_libraries (it adds artifact_dir just before the library loop and rewrites the package-only fallback), so whichever lands second has a small textual conflict in autoform_cli/skeleton.py (two hunks). Its build directory stays rooted at the package directory, as Lake's is, so the two changes do not interact. A resolution that leaves src_dir=root in the package-only fallback fails the package-only case of the new test.

No other open PR conflicts with this one. Merged onto current main, this change leaves every other open PR with the conflicts it already has.

Not in this PR

The freshness check still reports any failure of lake --rehash --no-build build other than stale artifacts with a headline about .lake needing to be writable. That headline is how the unknown target in the issue surfaced. This PR fixes the module mapping, not that message.

Closes #192.

[Deicyde]

Review at a8b3e16

Verdict: ready after PR-body edits; no code change needed. lean_libraries now joins the project root, the package srcDir and the library srcDir, which is what Lake v4.32.2 does (Package.srcDir and LeanLib.srcDir), and the package-only fallback uses the package srcDir. lake translate-config writes the package srcDir at the top level and each library's as configured, so nothing is joined twice. Projects that set srcDir only on the library, including those autoform project new creates and the bundled example, are unchanged. The real-Lean translate-config test ran in CI without skipping.

Required before merge

• Name the third consumer. autoform unused-hypotheses (from Add autoform unused-hypotheses: report hypotheses a proof never uses #198, merged after this branch was cut) also reads lean_libraries and places declarations through module_of, so it changes behavior too; the body names only skeleton and work impact.
• Say the test plan was narrowed. skeleton: lean_libraries ignores a package-level srcDir #192 asked for real-Lean coverage through both lakefile formats, and only lakefile.lean has it. lean_libraries parses lakefile.toml itself, so a real-Lean TOML test would run the same code as the unit test, and Lake's own nesting is already pinned by a real build in test_real_toml_build_uses_target_src_dir_globs_and_import_closure. The body should say so.

Optional

• An end-to-end regression for the reported symptom (unknown target src.Skel.Main), using the skeleton fixture with a package srcDir.
• Note Search a shared Lean library, generate its index, and teach the skills to reuse it (#203) #204 as another reader of lean_libraries; there is no conflict.

Decision for the maintainer

• Closing skeleton: lean_libraries ignores a package-level srcDir #192 leaves the misleading freshness headline with no open tracker: every non-stale failure of lake --rehash --no-build build is reported as a .lake writability problem, which is how this bug stayed hidden. File a focused issue for it, or say "Part of skeleton: lean_libraries ignores a package-level srcDir #192"?

Checked with an 11-layout driver, without Lean, on main and with the change: library-only layouts are unchanged, and every package-srcDir layout now maps to Proj. CI: all 9 checks pass.

The body edits are going in now; a follow-up comment will confirm.

Posted by PR swarm: Issue Triage

[Deicyde]

Review at a8b3e16

Verdict: Merge-ready. lean_libraries joined each library's srcDir onto the project root and ignored the package's srcDir, while Lake composes pkg.dir / pkg.srcDir / lib.srcDir. The PR reads the top-level srcDir (default .) once and uses it as the base for every library and for the package-only fallback (autoform_cli/skeleton.py:1240, :1246, :1261). On a project that sets srcDir on the package (which package p where srcDir := "src" in lakefile.lean produces through lake translate-config), autoform skeleton now extracts evidence and autoform work impact now measures impact; before, both failed closed and were unusable on that layout. With no package srcDir every path is unchanged, lean_libraries is the only parser of srcDir and both of its callers (skeleton.py:2055, impact.py:854) get the fix, and the new tests fail with either changed line reverted (confirmed by trace). The real-Lean CI job runs the new test with skipping disabled, so its pass confirms that lake translate-config writes the package srcDir as a top-level key.

Optional

• tests/test_skeleton.py:1147-1157 (confirmed by reading): the stubbed lakefile.lean test feeds lean_libraries the same TOML the library parametrization already covers, so it adds no coverage beyond the TOML and real-Lean tests. Drop it if you want fewer lines.
• autoform_cli/impact.py:248 (plausible gap): no tests/test_impact.py case covers a package-level srcDir; the impact fix is pinned only indirectly through the skeleton tests. A small impact test would pin it directly. Not blocking.
• The misleading freshness headline from skeleton: lean_libraries ignores a package-level srcDir #192 (a ".lake ... must be writable" message over an unrelated lake build failure) stays, as the PR body says. Nothing tracks it once skeleton: lean_libraries ignores a package-level srcDir #192 closes, so it is worth its own issue.

Landing

• Still a draft; mark it ready first. Closes skeleton: lean_libraries ignores a package-level srcDir #192.
• Merges cleanly onto current main. No ordering dependency on the other open PRs.
• One-line textual conflict with Allow proof imports with measured impact #183 in autoform_cli/skeleton.py: both rewrite the package-only fallback LeanLibrary(...) and the library append. Land this first and let Allow proof imports with measured impact #183 rebase over it, keeping Allow proof imports with measured impact #183's artifact_dir= and this PR's src_dir=package_src.resolve(). The two changes don't interact semantically, since Allow proof imports with measured impact #183's artifact_dir stays rooted at root / build_dir as Lake roots it.
• Search a shared Lean library, generate its index, and teach the skills to reuse it (#203) #204 adds a third caller of lean_libraries and picks up this fix with no conflict.

This was a static review: no tests were run locally. CI at this head: all 9 checks pass, but they ran before #165 merged into main, so update the branch (or rerun CI) before merging.

Posted by PR swarm: PR Swarm Lead

[Deicyde]

Changes since the review at a8b3e16

Description only; no code change. It now names autoform unused-hypotheses (from #198) as the third reader of lean_libraries, explains why the issue's real-Lean lakefile.toml test was not added (lean_libraries parses that file itself, and Lake's nesting is pinned by a real build in test_real_toml_build_uses_target_src_dir_globs_and_import_closure), and reports the CI result. The freshness-headline question stays open for you.

Posted by PR swarm: Issue Triage