lake failing because of camel casing overriding user intentions

[kim-em]

lakefile.lean:

import Lake
open Lake DSL

package «foo» {
  -- add any package configuration options here
}

@[default_target]
lean_lib «bar» {
  -- add any library configuration options here
}

(Note lowercase lean_lib name.)

• bar/A.lean empty
• bar/B.lean just containing import bar.A
• bar.lean just containing import bar.B

I think this is a valid setup, even if the choice of filename casing is contrary to standard usage.

However it currently fails:

% lake build
[0/1] Building Bar
error: > LEAN_PATH=./build/lib DYLD_LIBRARY_PATH=./build/lib /Users/kim/.elan/toolchains/leanprover--lean4---v4.1.0-rc1/bin/lean ./././Bar.lean -R ././. -o ./build/lib/Bar.olean -i ./build/lib/Bar.ilean -c ./build/ir/Bar.c
error: stdout:
./././Bar.lean:1:0: error: unknown package 'bar'
You might need to open '/Users/kim/scratch/foo' as a workspace in your editor
./././Bar.lean:4:13: error: unknown constant 'String'
error: external command `/Users/kim/.elan/toolchains/leanprover--lean4---v4.1.0-rc1/bin/lean` exited with code 1

Similarly opening either bar.lean or bar/B.lean in VSCode gives:

unknown package 'bar'
You might need to open '/Users/kim/scratch/foo' as a workspace in your editor

This is on both v4.1.0-rc1 and nightly-2023-09-19.

This is caused by multiple usages of toUpperCamelCase name in lake.

(From zulip.)