Weird project names in VS Code

Stream: lean4

[Anne Baanen]

I had a few students, who are newcomers to Lean, who created projects in VS Code with unusual names. The error handling isn't optimal:

• project named "LEAN": terminal reports "error: reserved package name" but they still get a directory containing Lean.lean so they didn't realize there was an error
• project named "demo.lean" and "My project": the extension keeps saying to restart the dependencies, but never building the files (but this doesn't replicate on my machine so unsure what specifically goes wrong)

[Eric Wieser]

There is a name resolution bug for project names containing periods that probably impacts demo.lean, though it's fixed upstream as of a day or two ago

[Eric Wieser]

Of course the generated project will have pretty wonky names, but it should at least work