reorder Lake help text

Stream: lean4

[Scott Morrison]

I recently made a proposal to reorder the presentation of the text in lake help, at lean4#2725.

Currently the help text shows options (e.g. --version, --dir) first, and then commands (e.g. new, build, ...). My proposal suggested putting the commands before the options. Further, my proposal suggested putting the most frequently used commands at the top of the list of commands.

There was then a discussion in which is was suggested that it was better and/or more standard to put the most important information last due to terminal scrolling. This discussion ended in disagreement and a request for a poll to help determine the right path.

[Scott Morrison]

/poll Preferred resolution of lean4#2725

[Jireh Loreaux]

I pipe help to less most of the time.

[Scott Morrison]

(For context it is currently 34 lines of text.)

[Kevin Buzzard]

They only time I ever see that text is when I type lake exe cache gt and then have to wait while lake thinks for ages (I'm too scared to hit ctrl-C) and then barfs it all out and then I can finally fix the typo

[Scott Morrison]

@Kevin Buzzard, the lake exe cache help text and the lake help text are unrelated.

[Scott Morrison]

We're taking about the later now.

[Scott Morrison]

The cache help text can be modified directly in Mathlib.

[Mario Carneiro]

Re: "produce no more than 1 page of help text, with either docs or a different flag for more in depth documentation", one nice (or possibly "a bit too clever" depending on your disposition) feature of clap (the standard rust CLI parser library) is that using myprog -h shows "short help" and myprog --help shows "long help"; these are primarily differentiated by using a paragraph (4-5 lines) per command/option instead of one line. (myprog alone is treated as an error, if this is a command with required subcommands, which can be configured to give the short help but by default just explains the error, shows the usage line and suggests to run help.)

[Jannis Limperg]

I would hate to see a distinction between -h and --help; there's a very strong expectation that these are synonyms (and generally that the short form and the long form of an option are synonyms).

Imo, a nice solution is to have --help invoke less automatically (if available and if stdout is a terminal). git does this for subcommands (git diff --help), though apparently not for git --help.

[Mac Malone]

Jannis Limperg said:

Imo, a nice solution is to have --help invoke less automatically (if available and if stdout is a terminal). git does this for subcommands (git diff --help), though apparently not for git --help.

Interesting. On Windows, git <command> --help opens all its hep text as HTML pages. git <command> -h produces command line output. git --help also produces CLI help and git -h is an error. (I had only ever seen the HTML pages before, so the other features are new surprise to me.) It also does not pipe it to less even when available (e.g., in MSYS2).

[Mac Malone]

(Apparently the "clever" distinction between -h and --help happens outside of clap. Still, I am not particularly sold on this wisdom of this.)

[Jannis Limperg]

On Linux, git clone --help acts as man git-clone. (Could be dependent on distribution packaging I guess; this is on Gentoo.)

[Pedro Sánchez Terraf]

Jannis Limperg said:

On Linux, git clone --help acts as man git-clone. (Could be dependent on distribution packaging I guess; this is on Gentoo.)

Same on Debian testing. Also, on Linux, I agree -h and --help should be synonyms. git clone -hspits out more than a full window of text.