binaries with autocompletion

Stream: lean4

[Arthur Paulino]

How to create executable binary files with tab autocompletion?
(I'm wondering how to create Lean cli apps with autocompletion)

[Henrik Böving]

If by autocompletion you are referrring to stuff like getting the ls options when typing ls -<TAB> that's the job of your shell and has to be set up in a shell dependent way for all programs. If you are talking about autocompletion in for example a REPL like program, that would be handled by readline stuff.

[Arthur Paulino]

I'll try to explain with an example. Suppose I want lake to autocomplete "build" for me when I type lake b<TAB>. How does that wiring work?