Imports not working for module names with dots

[ajs1998]

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

To import a file A/B.C.lean, import «A».«B.C» instead tries to find a file called A/B.lean.

The workaround was to use import «A».«B.C.lean» instead.

Context

Bug described here

Steps to Reproduce

1. Create a file A/B.C.lean
2. Try to import it from a different file with import «A».«B.C»

Expected behavior: Import works

Actual behavior:

`/home/vscode/.elan/toolchains/leanprover--lean4---v4.2.0/bin/lake print-paths Init «A».«B.C» --no-build` failed:

stderr:
error: '«A».«B.C»': no such file or directory (error code: 2)
  file: ./././A/B.lean

Versions

Lean v4.2.0

Additional Information

[Additional information, configuration or data that might be necessary to reproduce the issue]

Impact

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