Lake doesn't ensure that module roots are disjoint

[david-christiansen]

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 :+1: to issues you consider important. If others are impacted by this issue, please ask them to add :+1: to it.

[digama0]

Can we also lift this restriction? It is not very intuitive from the user's perspective, also as evidenced by the discussion.

[david-christiansen]

I think that it's reasonable for each library to have its own root(s), disjoint from all others. Otherwise, we could encounter large coordination problems, because adding a module to a library could break some other library that placed it in the same location. I don't think that's unintuitive.

[digama0]

I don't see how there are large coordination problems if the two libraries in question are in the same package, as in your example. The coordination problem only arises if these are libraries under different maintainers. But even then, this seems like an issue for lake to be dealing with, not lean.

I think that it's reasonable for each library to have its own root(s), disjoint from all others.

Moreover, this is not just about library roots being distinct: if package foo has library 1 at Foo.Lib1.* and library 2 at Foo.Lib2.* then this is still disallowed, because both libraries have the same root Foo, which is named after the package foo. To me this seems like (1) not a collision and (2) a perfectly reasonable thing for the foo package to do, and banning it makes no sense to me. In fact, it creates a perverse incentive where package foo now has to take multiple top level roots like Lib1.* and Lib2.* which are more likely to conflict with libraries from other packages because they lack the Foo prefix. Perhaps we would say that they should have been named FooLib1.* and FooLib2.* but in practice that's not how libraries are being named currently.

[Kha]

if package foo has library 1 at Foo.Lib1. and library 2 at Foo.Lib2. then this is still disallowed

I don't think it is?