RFC: lake should give a warning if a project is called `test`

[riccardobrasca]

Proposal

Lake should warn, with an overridable warning, when a new project is given a problematic name such as Test. We recently saw a fresh project depending on mathlib fail to compile because Lean resolved Test.Basic to Plausible.Test.Basic. A warning at project creation time, or at least a clearer error message, would make this much easier to understand and avoid.

More generally, lake could check if the name of the project is already "taken" by a dependency (for example if a project depending on mathlib is called batteries).

[bryangingechen]

Reproduction:

lake new test math-lax
cd test
lake build

Output:

✖ [3/6] Running Test.Basic
error: no such file or directory (error code: 4294967294)
  file: test/.lake/packages/plausible/Test/Basic.lean
Some required targets logged failures:
- Test.Basic
error: build failed

[tydeu]

This appears to have been a naming issue in plausible that was fixed in leanprover-community/plausible#58.

Did this occur on an old version of Lean or is Mathlib using an old version of Plausible?

In future, Lake will hopefully support private libraries to help avoid clashes like these.

[riccardobrasca]

Yes, the specific case of test is now fixed. It would be nice if lake could give a more informative error though.