Foo..lean works when `import`ed but not in vscode

Stream: lean4

[Eric Wieser]

If I create MyProject/Foo..lean by accident, then when opened in VSCode the extension complains it can't find MyProject/Foo.lean. However, I can import MyProject.«Foo.» in a downstream file and everything is happy there.

[Eric Wieser]

Hopefully no sane person would intentionally add this extra ., but an error message that tells me Lean is trying to read a different file to the one I have open in VSCode is very confusing.

[Eric Wieser]

docs#Lake.modOfFilePath seems to be the culprit

[Eric Wieser]

@Mac Malone, do you know if anything would break if the logic changed to "just strip the last extension"?

[Eric Wieser]

I ran into this again today with some filenames of the form Section_1.1.lean

[Eric Wieser]

Does it even make sense to call this function on any extension other than .lean?

[Mac Malone]

@Eric Wieser The opposite choice has its own problems. For example, modOfFilePath "Foo/Bar.olean.server" will return `Foo.Bar.olean , which is definitely not desirable.

[Eric Wieser]

What if the caller specified the relevant extension?

[Eric Wieser]

Or is the idea that the caller is just the command line recieving an arbitrary file?

[Eric Wieser]

In which case, it seems like you could drop extensions until you hit something in a known list of lean extensions, and fail with "not a module" otherwise

[Eric Wieser]

I guess the other way to fix this would be for the vscode extension to compute a module name rather than asking lake to guess it

[Mac Malone]

I think that dots in a file name (that do not indicate extensions) or a module name (as they already carry a special meaning) should not be encouraged or well-supported. More informative error messages; however, would certainly be nice.

[Eric Wieser]

I suspect it is easier to make this work than it is to make it propagate an error back to the vscode editor

[Mac Malone]

I am bit confused how the function leads to this error.

[Eric Wieser]

vscode is passing the full path to the file, then currently Section_1.1.lean is being stripped into the module name Section_1

[Mac Malone]

That I understand. I am confused, though, why that would cause an error. Lean/Lake and the server can sitll work on files that are not recognized modules.

[Eric Wieser]

What does "recognized module" mean?

[Eric Wieser]

The failure happens during setup-file, in case that helps

[Mac Malone]

One should be able to edit a file with any name with the Lean extension. For example, one can create a file called foo..baz and still edited it with Lean. Producing a incorrect module name should not cause an error.

[Mac Malone]

(From a quick test, it works for me.)

[Eric Wieser]

My guess is that something is saying "this ends in .lean so must be a module", and then something else is saying "Whoops I screwed up the name and the module doesn't exist)

[Eric Wieser]

Does foo..baz.lean work for you, inside a lean project?

[Mac Malone]

Yes, both foo..baz.lean and foo..lean work for me.

[Mac Malone]

While Lake may not correctly deduce the desired module name, it should just fall back to its default support for arbitrary files (i.e., the approach it uses for untitled VS Code files).

[Eric Wieser]

Well, I get

`/home/gitpod/.elan/toolchains/leanprover--lean4---v4.22.0-rc3/bin/lake setup-file /workspace/my_repo/MyProject/Paper/foo..baz.lean - --no-build --no-cache` failed:

stderr:
✖ [2/2] Running QuadraticAndBilinear.Paper.foo:setup
error: no such file or directory (error code: 2)
  file: /workspace/my_repo/MyProject/Paper/foo.lean
Some required builds logged failures:
- MyProject.Paper.foo:setup
error: build failed
All Messages (1)

[Eric Wieser]

Maybe this is fixed in the nightly

[Mac Malone]

No. The problem here is that the foo...baz.lean file is within a library directory. I forgot the Lake's filter here doesn't actually verify if a module within a library exists (in findModule?) -- it just checks for the right prefix.

[Mac Malone]

In that case, I think you are right, stripping exactly .lean from the module name is the most correct solution here (in LeanLib.findModuleBySrc?). As it will always add back exactly that extension.

[Mac Malone]

Hard-coding that findModuleBySrc? and not removing extensions at all in modOfFilePath seems like my probable fix.

[Eric Wieser]

Perhaps modOfFilePath should be renamed to modOfFilePathStem or something in that case?

[Mac Malone]

Or modOfFileStem. A rename sounds good.

[Eric Wieser]

Are you describing a change that is now (low?) on your TODO list, or saying that this is too niche an issue for you to spend any time on and telling me how to make a PR?

[Mac Malone]

Good point! I didn't make that very clear, did i? This is an issue I should be able to address quickly. Feel free to file issue if you would like to get a notification when I close it with a PR.