Inconsistent file naming across utils

Stream: general

[Yaël Dillies]

If I want to get cache for Data.Finset.Basic, I need to run lake exe cache get Mathlib/Data/Finset/Basic.lean. However if I to build it I need to run lake build Mathlib.Data.Finset.Basic

[Yaël Dillies]

Can we fix the inconsistency here?

[Michael Stoll]

(Maybe allow both spellings in both cases?)

[Anne Baanen]

I have a strong preference for file paths over dots, since file paths work with many external tools (like tab completion in my shell).

[Mauricio Collares]

Make sure to react-vote at lean4#2756 :)

[Johan Commelin]

I have a strong preference for allowing both spellings.

• Because in some situations I might want to copy a file path
• Because in some situations I might want to copy from an import statement

[Eric Wieser]

What if your filesystem contains Foo.Bar.lean and Foo/Bar/lean.lean?

[Eric Wieser]

Maybe the answer is an -m flag for "module" (or -f for file) that switches from filepath to importpath mode

[Johan Commelin]

Happy with that

[Johan Commelin]

I just think that both scenarios are very common, and it would be very helpful if both are supported.

[Mauricio Collares]

Eric Wieser said:

Maybe the answer is an -m flag for "module" (or -f for file) that switches from filepath to importpath mode

The ergonomic option, in my opinion, would be to have flags for both and let the flag-less version guess what the user meant, possibly erroring out if both options are valid for the given input.