Capitalising filenames breaks imports between files

Prerequisites

• Put an X between the brackets on this line if you have done all of the following:
  • Checked that your issue isn't already filed.
    • Specifically, check out the wishlist, open RFCs,
      or feature requests.
  • Reduced the issue to a self-contained, reproducible test case.

Description

Changing the filename of a .lean file by just capitalising or uncapitalising is not picked up by the lean server (in vs code at least), and this results in it not recognising when the contents of an imported file have changed.

Steps to Reproduce

This was only tested in VS code. I don't know how to use emacs.

1. leanproject new bugtest
2. create src/file1.Lean and src/file2.lean (pay attention to capitalisation)
3. in file2.lean put import file1
4. Rename file1.Lean to file1.lean (remove the capitalisation), either in vs-code's browser or elsewhere
5. Observe vs-code does not detect this change in the opened tab-name (this can be fixed by reopening the tab, but regardless the following issues still occur)
6. Put def foo : ℕ := 3 in file1.lean
7. do #check foo in file2.lean and observe it doesn't recognise it.
8. Restart the lean server and observe it now recognises it
9. Make any change to file1.lean (like change the type of foo or just delete foo) and observe it doesn't update in file2.lean until the lean server or vs code is restarted (after which the problem still persists upon further changes).

There seems to be nothing you can do to fix this broken import relationship. I got it working again by changing the file name of file1.lean beyond capitalisation, say to file0.lean, and then the import relationship is fixed again, once the import is changed to import file0.

This issue also occurs when capitalising or uncapitalising other parts of the filename, say File1.lean vs file1.lean, which is arguably more likely to occur. Even after changing import File1 to import file1, the same problems occur.

Note also that the Infoview tab says the old, capitalised filename at the top throughout this process.

Expected behavior: [What you expect to happen]

Changes in file1.lean to be seen by the lean server.

Actual behavior: [What actually happens]

No changes recognised until lean server is restarted

Reproduces how often: [What percentage of the time does it reproduce?]

100% of the time

Versions

Lean (version 3.15.0, commit 56f8877f1efa, Release)

Mac OS Catalina 10.15.5

Reproduce the issue with leanproject new bugtest in VS Code, using src/file1.Lean, src/file2.lean, and the import file1 relationship described in the report. Start by tracing how the Lean server tracks renamed files and imports; done means capitalization-only renames update the open tab and imported-file changes without restarting the server.