autocomplete module names with `lake build`

Stream: lean4

[Matthew Ballard]

Is there any way that I can easily get lake build Mathlib.Ri… to auto-complete?

[Julian Berman]

I wrote a simple version for zsh here: https://github.com/Julian/dotfiles/blob/main/.config/zsh/completions/_lake

[Julian Berman]

There's an earlier thread where it was briefly discussed, obviously I haven't made that anything more than a POC otherwise I'd upstream it assuming the maintainers are amenable, but it should work for that specific case.

[Mario Carneiro]

This relates to lean4#2756 , since using file name syntax would allow the shell's native autocompletion to work

[Matthew Ballard]

I would prefer that yes