This is not directly related to the backends, but the website: It is standard to name Lean files all lowercase, e.g. defs.lean, submission.lean. When downloading a Lean zip file, e.g. this one, the Lean files are automatically capitilised though, e.g. Defs.lean, Submission.lean. This causes the imports for users to fail and they have to rename the downloaded files first. See, for example, this Zulip post.
This is not directly related to the backends, but the website: It is standard to name Lean files all lowercase, e.g.
defs.lean,submission.lean. When downloading a Lean zip file, e.g. this one, the Lean files are automatically capitilised though, e.g.Defs.lean,Submission.lean. This causes the imports for users to fail and they have to rename the downloaded files first. See, for example, this Zulip post.