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

autoform_cli/skeleton.py

@@ -1216,6 +1216,9 @@ def lean_libraries(lean_root: str | Path) -> tuple[LeanLibrary, ...]:
     workflow reads the root package name, so both manifest languages are
     handled without a second parser for Lean syntax. When both exist, Lake
     builds from ``lakefile.lean``, so that is the one read here too.
+
+    As in Lake, a library's ``srcDir`` is relative to the package's ``srcDir``,
+    which is also the source directory of a package without library targets.
     """
 
     root = Path(lean_root).expanduser().resolve()
@@ -1234,12 +1237,13 @@ def lean_libraries(lean_root: str | Path) -> tuple[LeanLibrary, ...]:
             [f"cannot safely parse the Lake configuration of {root}: it exceeds the parser's limits"]
         ) from exc
 
+    package_src = root / str(config.get("srcDir", "."))
     libraries: list[LeanLibrary] = []
     for entry in config.get("lean_lib", []) or []:
         if not isinstance(entry, dict) or not isinstance(entry.get("name"), str):
             continue
         name = entry["name"]
-        src_dir = root / str(entry.get("srcDir", "."))
+        src_dir = package_src / str(entry.get("srcDir", "."))
         roots = entry.get("roots")
         if not isinstance(roots, list) or not all(isinstance(item, str) for item in roots):
             roots = [name]
@@ -1254,7 +1258,7 @@ def lean_libraries(lean_root: str | Path) -> tuple[LeanLibrary, ...]:
     if not libraries:
         package = config.get("name")
         if isinstance(package, str) and package:
-            libraries.append(LeanLibrary(name=package, src_dir=root, roots=(package,)))
+            libraries.append(LeanLibrary(name=package, src_dir=package_src.resolve(), roots=(package,)))
     if not libraries:
         raise SkeletonError([f"the Lake configuration of {root} declares no library"])
     return tuple(libraries)

tests/test_skeleton.py

@@ -1023,6 +1023,31 @@ def test_a_package_without_library_targets_is_its_own_library(tmp_path: Path) ->
     assert library.src_dir == project.resolve()
 
 
+@pytest.mark.parametrize(
+    ("lakefile", "src_dir"),
+    [
+        pytest.param(
+            'name = "proj"\nsrcDir = "pkgsrc"\n\n[[lean_lib]]\nname = "Proj"\nsrcDir = "lib"\n',
+            "pkgsrc/lib",
+            id="library",
+        ),
+        pytest.param('name = "Proj"\nsrcDir = "pkgsrc"\n', "pkgsrc", id="package-only"),
+    ],
+)
+def test_libraries_nest_under_the_package_source_directory(tmp_path: Path, lakefile: str, src_dir: str) -> None:
+    project = tmp_path / "project"
+    (project / src_dir).mkdir(parents=True)
+    (project / "lakefile.toml").write_text(lakefile, encoding="utf-8")
+    (project / src_dir / "Proj.lean").write_text("", encoding="utf-8")
+
+    libraries = lean_libraries(project)
+
+    # Lake joins a library's srcDir onto the package's srcDir, not onto the project root.
+    assert libraries[0].src_dir == (project / src_dir).resolve()
+    assert module_of(project / src_dir / "Proj.lean", libraries) == "Proj"
+    assert path_of("Proj", libraries, project) == f"{src_dir}/Proj.lean"
+
+
 @pytest.mark.parametrize(
     "toml_11",
     [
@@ -1107,6 +1132,31 @@ def test_a_failed_translation_reports_the_error_rather_than_lakes_info_line(tmp_
     assert caught.value.issues == (f"lake translate-config failed: {error}",)
 
 
+def _project_with_a_package_source_directory(tmp_path: Path) -> Path:
+    """lakefile.lean puts the package's sources under ``pkgsrc`` and gives its library no srcDir of its own."""
+
+    project = tmp_path / "project"
+    project.mkdir()
+    shutil.copy(_FIXTURE / "lean-toolchain", project / "lean-toolchain")
+    (project / "lakefile.lean").write_text(
+        'import Lake\nopen Lake DSL\n\npackage proj where\n  srcDir := "pkgsrc"\n\nlean_lib Proj\n', encoding="utf-8"
+    )
+    return project
+
+
+def test_lakefile_lean_libraries_nest_under_the_package_source_directory(tmp_path: Path, monkeypatch) -> None:
+    project = _project_with_a_package_source_directory(tmp_path)
+    # lake translate-config writes the package's srcDir as a top-level key.
+    monkeypatch.setattr(
+        "autoform_cli.skeleton._translate_lakefile",
+        lambda _root: b'name = "proj"\nsrcDir = "pkgsrc"\n\n[[lean_lib]]\nname = "Proj"\n',
+    )
+
+    (library,) = lean_libraries(project)
+
+    assert (library.name, library.src_dir) == ("Proj", project.resolve() / "pkgsrc")
+
+
 def test_a_project_without_a_lakefile_is_refused(tmp_path: Path) -> None:
     with pytest.raises(SkeletonError):
         lean_libraries(tmp_path)
@@ -2224,6 +2274,15 @@ def test_lakefile_lean_wins_through_lake_translate_config(tmp_path: Path) -> Non
     assert (library.name, library.src_dir, library.roots) == ("FromLean", project.resolve() / "lean-src", ("LeanRoot",))
 
 
+@pytest.mark.skipif(not _lean_toolchain_available(), reason="needs lake and the fixture's Lean toolchain")
+def test_package_source_directory_nests_libraries_through_lake_translate_config(tmp_path: Path) -> None:
+    project = _project_with_a_package_source_directory(tmp_path)
+
+    (library,) = lean_libraries(project)
+
+    assert (library.name, library.src_dir) == ("Proj", project.resolve() / "pkgsrc")
+
+
 def test_required_real_lean_tests_fail_closed(monkeypatch: pytest.MonkeyPatch) -> None:
     monkeypatch.setenv("AUTOFORM_REQUIRE_REAL_LEAN_TESTS", "1")
     monkeypatch.setattr(shutil, "which", lambda _name: None)