Bad file names lead to mysterious lake error messages

Prerequisites

• Put an X between the brackets on this line if you have done all of the following:
  • Check that your issue is not already filed.
  • Reduce the issue to a minimal, self-contained, reproducible test case. Avoid dependencies to mathlib4 or std4.

Description

Having a forbidden character in a file name leads to a misleading error message.

Context

This was discussed at least here and there. It affected Terence Tao there.

Steps to Reproduce

Create a project foo containing Foo/main-lemmas.lean and Foo/main.leanand put import Foo.main-lemmas in Foo/main.lean.

Expected behavior: [Clear and concise description of what you expect to happen]

The ideal behavior would be: everything works. An acceptable situation would be an error message saying Foo.main-lemmas is not a valid name for a Lean file and the file should be renamed or used with French quotes.

Actual behavior: [Clear and concise description of what actually happens]

The error message is

error: build cycle detected:
  +Foo.main:lean.precompileImports
  +Foo.main:lean.precompileImports

(both when invoked from the command line and from VSCode).

Versions

Lean (version 4.3.0-rc1, commit baa4b68a7192, Release)
Linux

Additional Information

This is first a parsing error. The import parsing stops before the dash and sees a circular import of Foo.main in Foo.main.

Impact

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

Reproduce the issue with Foo/main.lean importing Foo.main-lemmas, using both the command line and VSCode as described. Trace the import parsing and build-cycle diagnostic paths; done means a forbidden filename produces a clear naming error or otherwise works instead of reporting a mysterious cycle.