bash completion

Stream: lean4

[Yury G. Kudryashov]

Is there bash/csh/zsh/whatever file that enables shell completion for lake? I'm specifically interested in completing existing targets for lake build. If there is no such file, is there a lean/lake command that prints all available targets or the best option is to run find . -name lake-packages -prune -name *.lean | sed ...?

[Julian Berman]

I wrote a POC one for zsh in my dotfiles here. I don't know if there's a more complete one someone's written at this point.

[Julian Berman]

(It's very very barebones, and came up only when there was some discussion over completing lean modules vs filenames -- but it should be pretty easily extensible if you find nothing better.)

[Yury G. Kudryashov]

Does it complete lake build ...?

[Julian Berman]

No it's mostly just the zsh skeleton -- I don't immediately see a way to list all the possible targets from the command line, it looks like one would have to call into some Lake internals from within Lean, maybe like getWorkspace and then the various *facetConfig fields are them (though certainly I'm no Lake expert). I'm not sure I'll have any time to try to figure it out on the Lean side but if it's any use once it's clear what to run I'm happy to plumb it into that completion script.