feat: lake: resolve module clashes on import

[tydeu]

This PR adds a module resolution procedure to Lake to disambiguate modules that are defined in multiple packages.

On an import, Lake will now check if multiple packages within the workspace define the module. If so, it will verify that modules have sufficiently similar definitions (i.e., artifacts with the same content hashes). If not, Lake will report an error.

This verification is currently only done for direct imports. Transitive imports are not checked for consistency. An overhaul of transitive imports will come later.

[leanprover-community-bot]

Mathlib CI status (docs):

• ❗ Mathlib CI can not be attempted yet, as the nightly-testing-2025-11-19 tag does not exist there yet. We will retry when you push more commits. If you rebase your branch onto nightly-with-mathlib, Mathlib CI should run now. You can force Mathlib CI using the force-mathlib-ci label. (2025-11-20 04:02:33)
• ✅ Mathlib branch lean-pr-testing-11270 has successfully built against this PR. (2025-11-22 00:13:50) View Log

[leanprover-bot]

Reference manual CI status:

• ❗ Reference manual CI can not be attempted yet, as the nightly-testing-2025-11-19 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. (2025-11-20 04:02:35)
• ❗ Reference manual CI can not be attempted yet, as the nightly-testing-2025-11-21 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. (2025-11-21 23:06:02)

[tydeu]

!bench

[leanprover-radar]

Benchmark results for 9a712ef against 6118662 are in! @tydeu

Major changes (2)

• lake build no-op//instructions changed by +13.0% (🟥).
• stdlib//instructions changed by +7.3% (🟥).

[tydeu]

!bench

[leanprover-radar]

Benchmark results for 6ba80e2 against 6118662 are in! @tydeu

Major changes (2)

• lake build no-op//instructions changed by +27.0% (🟥).
• stdlib//instructions changed by +7.3% (🟥).

[tydeu]

!bench

[leanprover-radar]

Benchmark results for 6e151c6 against 6118662 are in! @tydeu

Major changes (1)

• stdlib//instructions changed by +7.3% (🟥).

Minor changes (1)

• channel.lean//instructions changed by +0.5% (🟥).