cache glob regression

Stream: mathlib4

[Yaël Dillies]

It seems that lake exe cache get Foo/Bar/*.lean now downloads only the files that are directly in Foo/Bar and not files in subfolders (so eg it won't download cache for Foo.Bar.Baz). I noticed something had changed, but it took me a while to pinpoint what. Hence I would situate the change of behavior to around v4.7.0.

[Sebastian Ullrich]

Globs are resolved by your shell, not cache. Some shells understand Foo/Bar/**/*.lean.

[Yaël Dillies]

Uh, this is becoming really annoying syntax when all I want to do is to download cache for the files I have opened in the editor

[Richard Osborn]

For bash, you just need to set globstar with shopt -s globstar. Recursive globbing is on by default in zsh.

[Mario Carneiro]

Just in case it wasn't clear, I don't think this changed any time recently, since there is no way it could unless you happen to have changed shells or shell options around v4.7.0. Another consideration: if you have a file in the Foo/Bar folder which imports the others (i.e. you have all 'default.lean' equivalent files), then using only Foo/Bar/*.lean will build those other files as well, since cache will automatically take the dependency closure of the files you supply.