Lake: path dependencies should share build artifacts with parent workspace

Problem

When a sub-project uses a path dependency to its parent (e.g. require Foo path = ".."), Lake creates a fully independent .lake/ directory with its own copies of all transitive dependencies. This means:

1. Mathlib oleans must be fetched/built twice — once for the root workspace, once for the sub-project, even though both resolve to the same revision.
2. Multi-GB cache duplication — the sub-project's .lake/ is dominated by identical copies of the parent's dependencies.

Reproduction

project/
├── lakefile.toml          # requires Mathlib (transitively)
├── lake-manifest.json
├── .lake/                 # root workspace
│   └── packages/mathlib/  # oleans fetched via `lake exe cache get`
└── docs/
    ├── lakefile.toml      # requires project via `path = ".."`
    ├── lake-manifest.json
    └── .lake/             # independent workspace
        └── packages/mathlib/  # NO oleans, must fetch again or rebuild

Running lake build in docs/ cannot reuse the already-built Mathlib from ../.lake/packages/mathlib/.

Current workaround (CI)

# Root: lean-action handles Mathlib cache
- uses: leanprover/lean-action@v1
  with:
    use-mathlib-cache: "true"

# Sub-project: must fetch cache separately
- working-directory: docs
  run: |
    lake resolve-deps
    lake exe cache get || true  # fetch Mathlib oleans AGAIN
    lake build

Desired behavior

When a workspace has require Foo path = "..", Lake should be able to resolve Foo's transitive dependencies through the parent's .lake/ rather than cloning and building them independently. This would:

• Eliminate redundant Mathlib downloads/builds
• Share pre-built oleans across workspaces that pin the same revisions
• Reduce CI cache sizes significantly

Related

• #5342 — RFC: lake fetch command (for fetching without building)

Context

This pattern is common for Lean projects with Verso documentation sub-projects that import the parent library to generate cross-referenced docs.

Start by reproducing the setup in the root and docs lakefile.toml and lake-manifest.json files, then compare the two .lake directories. Run lake resolve-deps, lake exe cache get, and lake build from docs after preparing the root workspace. Done means the sub-project reuses the parent workspace's matching Mathlib artifacts without downloading or building duplicate copies.