Lake doesn't ensure that module roots are disjoint

Description

Lake allows the definition of library configurations that cannot reliably work because their roots overlap.

In particular, I can define the following configurations with no warnings or errors in the Lakefile:

import Lake
open Lake DSL

package "lib1" where

lean_lib «AB» where
  srcDir := "src/ab"
  roots := #[`A]

lean_lib «AC» where
  srcDir := "src/ac"
  roots := #[`A]

Running lake build results in an error that a file can't be found:

]> lake build
✖ [?/?] Computing build jobs
error: no such file or directory (error code: 2)
  file: ./././src/ac/A/B.lean
Some required builds logged failures:
- Computing build jobs
error: build failed

Setting the second root to A.C allows a successful build.

When one root subsumes another, the results of import become difficult to predict.

Context

This came up during out-of-band discussion surrounding #4962.

Steps to Reproduce

There's a few related issues here that I think are all symptoms of the same missing error message.

To reproduce the issue of two libraries having the same root:

1. Check out https://github.com/david-christiansen/demo-deeper-roots/tree/conflicting-roots
2. In Lib1/, run lake build

To reproduce the issue of one subsuming another:

1. Check out https://github.com/david-christiansen/demo-deeper-roots/tree/subsuming-roots
2. In Lib2/, run lake build
3. It succeeds, with the A.D from library ab being used (see Lib2/Other.lean to verify)

Expected behavior:

In both cases, I'd expect an error message in my editor when working on Lib1/lakefile.lean that the provided module root sets conflict with each other. I'd also expect that Lake would provide an error message when I attempt to build it.

At elaboration time, I'd expect the definition of library AC to have a message like:
AC's root 'A' conflict's with AB's root 'A'.

When running a build, assuming the elaboration-time error of the Lake configuration was not fatal, I'd expect something like:

The configuration in lakefile.lean describes multiple libraries whose root modules conflict. In particular, library 'AB' has root 'A', and 'AC' has root 'A'.

or

The configuration in lakefile.lean describes multiple libraries whose root modules conflict. In particular, library 'AB' has root 'A', and 'AC' has root 'A.C'.

Actual behavior:

When the roots are identical, there are confusing messages about "No such file". When they are not, but one subsumes the other, the results of importing modules from the package's libraries are difficult to predict.

Versions

"4.12.0-nightly-2024-08-16"

macOS 14.6.1

Impact

Add 👍 to issues you consider important. If others are impacted by this issue, please ask them to add 👍 to it.

Reproduce the conflicting-root cases from the linked demo-deeper-roots branches by running lake build in Lib1 and Lib2, then inspect the corresponding lakefile.lean definitions and Lake DSL library configuration. Done means both identical and subsuming module roots produce a clear conflict diagnostic during elaboration or build instead of a missing-file error or unpredictable import behavior.