The help message of Lean command line

Stream: lean4

[Shuhao Song]

The help message of Lean command line contains

--o=oname -o create olean file

This may lead to misunderstanding that the command needs both argument --o=oname and -o, i. e. lean --o=test.o -o test.lean. In the help message of GNU coreutils, such as ls, it is -a, --all ..., which might be better. I did my modification on my own fork https://github.com/leanprover/lean4/compare/master...meow-sister:lean4:cmdline_help_docstring. Is this suitable for a PR?

[Mac Malone]

@Shuhao Song You don't need both options. Using either --o or -o will work.

[Kyle Miller]

@Mac Malone Shuhao understands that, the question is whether to change the help output to make that clear

[Kyle Miller]

It seems other programs use commas to separate the different variants. For example, I just took a look at gsed -h and saw

  -n, --quiet, --silent
                 suppress automatic printing of pattern space
      --debug
                 annotate program execution
  -e script, --expression=script
                 add the script to the commands to be executed
  -f script-file, --file=script-file
                 add the contents of script-file to the commands to be executed

[Mac Malone]

Ah, sorry for the misunderstanding. :man_facepalming:

[Mac Malone]

Lake also uses commas.

[Kim Morrison]

Shuhao Song said:

Is this suitable for a PR?

@Shuhao Song, yes please. Please include in the PR description the explanation that this formatting is standard for other tools.

[Shuhao Song]

Kim Morrison said:

Shuhao Song said:

Is this suitable for a PR?

Shuhao Song, yes please. Please include in the PR description the explanation that this formatting is standard for other tools.

It was already merged