Import file with multiple dots in file name

Stream: lean4

[Alex Sweeney]

I'm trying to import a file in Functional Programming in Lean/5.0.lean
I was under the impression that if you surround your strings with \f<< and \f>> then it automatically escapes characters that would normally create issues, like spaces. But it seems to not work in this case

import «Functional Programming in Lean».«5.0»


`/home/vscode/.elan/toolchains/leanprover--lean4---v4.2.0/bin/lake print-paths Init «Functional Programming in Lean».«5.0» --no-build` failed:

stderr:
error: '«Functional Programming in Lean».«5.0»': no such file or directory (error code: 2)
  file: ./././Functional Programming in Lean/5.lean

It's trying to find a file called 5.lean instead. Renaming the file and import to 5-0.lean works, but obviously not ideal. Is there a different syntax I can use to support importing a file with multiple .s in its name?

[Eric Wieser]

This looks like a bug to me

[Eric Wieser]

import «Functional Programming in Lean».«5.0.lean» appears to work

[Mario Carneiro]

is this a lean issue or a lake issue?

[Eric Wieser]

This is a lean issue

[Eric Wieser]

lean --deps also drops the .0

[Eric Wieser]

Also, you can import the same module twice which makes Lean unhappy:

import Mathlib.ohno
import Mathlib.«ohno.lean»

(because the definitions already exist)

[Mac Malone]

This is because Lean uses withExtension to manipulate the file extensions of imports (e.g., to add .lean). This replaces the final "extension" (i.e., .0) if there is one.

[Eric Wieser]

What is it calling withExtension on?

[Eric Wieser]

Arguably putting Functional Programming in Lean/5.0 in a FilePath object in the first place is a mistake, because that doesn't represent an actual path

[Mac Malone]

Many things. For example, modToFilePath uses withExtension.

[Mac Malone]

Similarly, so does findWithExt. Most of the module loading code in Lean and Lake does.

[Eric Wieser]

That should be

def modToFilePath (base : FilePath) (mod : Name) (ext : String) : FilePath :=
  go mod
where
  go : Name → FilePath
  | Name.str p h => go p / (h + "." + ext) -- does `ext` include the `.`?
  | Name.anonymous => base
  | Name.num _ _ => panic! "ill-formed import"

right?

[Mac Malone]

Something like that would fix this, yes. I am a little curious as to why all of this code used withExtension in the first place. It struck me as weird when I first read it, but I kind of assumed there was a reason (as doing otherwise is just as easy) so I followed the pattern in Lake.

[Eric Wieser]

findWithExt looks safe until someone makes a package with a bizarre name

[Mac Malone]

Note that a findWithExt package is not a Lake package, it is just a root module name. So it would, e.g., break import «Foo-2.0» of the file Foo-2.0.lean.

[Alex Sweeney]

One more thing I want to add here.

import «Functional Programming in Lean».«5.0.lean» appears to work

That "worked" meaning it seemed like it could find the 5.0.lean file, but it gave a different error unknown package 'sandbox'. This is what my lakefile looked like.

import Lake
open Lake DSL

require mathlib from git
  "https://github.com/leanprover-community/mathlib4" @ "v4.2.0"

package «sandbox» {
  -- add package configuration options here
}

@[default_target]
lean_exe «Sandbox» {
  root := `Sandbox.Sandbox
}

lean_lib «Functional Programming in Lean» {
  globs := #[.submodules `«Functional Programming in Lean»]
}

And I had the top level folder Functional Programming in Lean/ with the x.y.lean chapter files. I renamed the directory and the lib and import to FPIL and import «FPIL».«5.0.lean» and the error went away and the import works fine now. I don't know if this is related to the original issue with . not being properly escaped, but it seems like a different bug since I only changed the directory name which only includes spaces.

[Eric Wieser]

I drafted a fix at lean4#2994

[Patrick Massot]

Do we really want to fix this? Shouldn't we simply say that such a file name is a bad idea?

[Alex Sweeney]

I can't remember where I read/heard it, but I thought the whole purpose of \f<< ... \f>> was to make it easier for less computer-literate mathematicians to start using Lean. I'm a software engineer and I understand why spaces and dots in directory/file names aren't normally used for programming projects. But I also understand that some new Lean users might not get that and think Lean ought to be able to handle it.

Normally I'd agree and say these are weird names and should be avoided, but I thought that was why \f<< \f>> existed in the first place.

[Scott Morrison]

I think that pretending we have support for disallowed names via \f<< \f>> is more trouble than it is worth. It encourages people to do the bad thing (not use plain vanilla names).

[Mario Carneiro]

Patrick Massot said:

Do we really want to fix this? Shouldn't we simply say that such a file name is a bad idea?

These two are not mutually exclusive, and we should do both

[Eric Wieser]

I think it's pretty clear that this is just a bug? The patch in lean4#2994 (once I actually get it working) is computationally faster anyway.

[Mac Malone]

Scott Morrison said:

I think that pretending we have support for disallowed names via \f<< \f>> is more trouble than it is worth. It encourages people to do the bad thing (not use plain vanilla names).

We are hopefully not pretending. \f<< \f>> names are certainly meant to be supported.

[Scott Morrison]

I mean, this thread wouldn't exist if disallowed names were supported. :-)

[Scott Morrison]

(That is, by claiming to support bad names, we have encouraged people to use them, thereby discovering the bugs in our handling of bad names!)

[Mario Carneiro]

Scott Morrison said:

I mean, this thread wouldn't exist if disallowed names were supported. :-)

"Supported" implies intent, and I believe the intent exists even if the implementation is lacking

[Mac Malone]

It is also worth noting that \f<< \f>> names are useful for more than just "bad" names. They also enable a wide variety of other useful non-identifier names (e.g., names in foreign languages with characters outside Lean's restricted identifier set).

[Eric Wieser]

lean4#2994 is now green. @Alex Sweeney, could you file a bug report on the lean4 issue tracker so that I can reference it from my PR?

[Alex Sweeney]

@Eric Wieser I haven't submitted an issue here before, so let me know if I need to change anything. I won't be available again until later tonight though.

https://github.com/leanprover/lean4/issues/2999