Case insensitivity can lead to lake builds which succeed when done "incrementally" but fail done together

[Julian]

Prerequisites

Please put an X between the brackets as you perform the following steps:

• [x] Check that your issue is not already filed: https://github.com/leanprover/lean4/issues
• [x] Reduce the issue to a minimal, self-contained, reproducible test case. Avoid dependencies to Mathlib or Batteries.
• [x] Test your test case against the latest nightly release, for example on https://live.lean-lang.org/#project=lean-nightly (You can also use the settings there to switch to “Lean nightly”)

Description

Given a module Foobar/baz.lean, an import spelled import FooBar.Baz (instead of import Foobar.Baz) can produce either a confusing error message or a successful build if done in 2 parts.

Context

I typoed the name of my package, and misattributed why it wasn't building correctly due to the error message.

Steps to Reproduce

Here's a full reproducer, only confirmed macOS, but perhaps which reproduces on any case-insensitive filesystem:

rm -rf Casesensitive && \
  lake new Casesensitive lib && \
  printf 'import CaseSensitive.Basic\n' >>Casesensitive/Casesensitive/Boom.lean && \
  printf 'Both imports, blows up:\n\n\n' && \
  printf '\nimport Casesensitive.Boom\n' >>Casesensitive/Casesensitive.lean && \
  (cd Casesensitive && \
  rm -rf .lake && \
  lake build); printf 'Good import then bad import, builds successfully:\n\n\n' && \
  printf 'import Casesensitive.Basic\n' >Casesensitive/Casesensitive.lean && \
  (cd Casesensitive && \
  lake build && \
  printf 'import Casesensitive.Boom\n' >Casesensitive.lean && \
  lake build && \
  printf '\nimport Casesensitive.Boom\n' >>Casesensitive.lean && \
  lake build)

where what the reproducer does is:

• create a package
• typo an import
• first build the package with a Casesensitive.lean target containing both, which fails
• then build it incrementally first with the working file then a second time with both imports in Casesensitive.lean -- (in my "real scenario" this is precisely what happened, as the file I typoed was a new file I was adding and adding to my build)

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

An import error saying CaseSensitive does not exist, even though I'm on a case insensitive filesystem, similar to the message produced on Linux which says CaseSensitive is an unknown prefix. (Ideally it could also hint that Casesensitive does, which could be used even for other minor typos and not just case sensitivity issues).

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

A cryptic error: ././././Casesensitive/Boom.lean:1:0: object file '././.lake/build/lib/CaseSensitive/Basic.olean' of module CaseSensitive.Basic does not exist if the build is done simultaneously (this is cryptic because it's not clear to the user whose fault it is that that file doesn't exist)

If building incrementally, the build succeeds.

Versions

[Output of #eval Lean.versionString] 4.12.0, commit [OS version, if not using live.lean-lang.org.] macOS 15.0

Additional Information

#2129 is related and may have the same underlying fix -- I've seen errors like that one as well when playing around a bit with ordering of the commands.

Impact

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