Arguably this is ill-defined; is Foo.Bar.lean a reference to ./Foo.Bar.lean or Foo/Bar/lean.lean?

(maybe the answer is to allow a leading ./ to disambiguate)

currently it's a reference to ./Foo.Bar.lean especially since Mathlib.lean should be parsed that way. One add ./ but requiring it would not work for Mathlib.lean

Would it be desired to just try out both options with something like to following?

  if arg.extension == "lean" then
    let mut mods := #[]

    -- try if a file `Foo/Bar/lean.lean` exists
    let mod := argₛ.toName
    let sourceFile ← Lean.findLean sp mod
    if ← sourceFile.pathExists then
      mods := mods.append #[(mod, sourceFile)]

    -- try if a file `./Foo.Bar.lean` exists
    let mod₂ : Name := arg.withExtension "" |>.components.foldl .str .anonymous
    if (← arg.pathExists) then
      mods := mods.append #[(mod₂, arg)]
    return .ok mods

Arguably this is ill-defined; is Foo.Bar.lean a reference to ./Foo.Bar.lean or Foo/Bar/lean.lean?

Alternatively, just assume that no one is going to do this. If they do, they can file a bug report, and we can tell them to stop being annoying. :-)

At any rate we should make sure what we implement is consistent with whatever lean4#2756 decides.