From 2d09c96caf480e5232a9c4446ba8fe35544ac694 Mon Sep 17 00:00:00 2001 From: Shuhao Song Date: Mon, 5 Aug 2024 06:54:34 +0800 Subject: [PATCH] chore: cli help text: comma-separate alternative option forms (#4911) 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. Some discussion is on Zulip thread [https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/The.20help.20message.20of.20Lean.20command.20line](https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/The.20help.20message.20of.20Lean.20command.20line). --- src/util/shell.cpp | 67 +++++++++++++++++++++++----------------------- 1 file changed, 34 insertions(+), 33 deletions(-) diff --git a/src/util/shell.cpp b/src/util/shell.cpp index 779c682b89..6310c9cc81 100644 --- a/src/util/shell.cpp +++ b/src/util/shell.cpp @@ -191,43 +191,44 @@ static void display_features(std::ostream & out) { static void display_help(std::ostream & out) { display_header(out); std::cout << "Miscellaneous:\n"; - std::cout << " --help -h display this message\n"; - std::cout << " --features -f display features compiler provides (eg. LLVM support)\n"; - std::cout << " --version -v display version number\n"; - std::cout << " --githash display the git commit hash number used to build this binary\n"; - std::cout << " --run call the 'main' definition in a file with the remaining arguments\n"; - std::cout << " --o=oname -o create olean file\n"; - std::cout << " --i=iname -i create ilean file\n"; - std::cout << " --c=fname -c name of the C output file\n"; - std::cout << " --bc=fname -b name of the LLVM bitcode file\n"; - std::cout << " --stdin take input from stdin\n"; - std::cout << " --root=dir set package root directory from which the module name of the input file is calculated\n" - << " (default: current working directory)\n"; - std::cout << " --trust=num -t trust level (default: max) 0 means do not trust any macro,\n" - << " and type check all imported modules\n"; - std::cout << " --quiet -q do not print verbose messages\n"; - std::cout << " --memory=num -M maximum amount of memory that should be used by Lean\n"; - std::cout << " (in megabytes)\n"; - std::cout << " --timeout=num -T maximum number of memory allocations per task\n"; - std::cout << " this is a deterministic way of interrupting long running tasks\n"; + std::cout << " -h, --help display this message\n"; + std::cout << " -f, --features display features compiler provides (eg. LLVM support)\n"; + std::cout << " -v, --version display version number\n"; + std::cout << " --githash display the git commit hash number used to build this binary\n"; + std::cout << " --run call the 'main' definition in a file with the remaining arguments\n"; + std::cout << " -o, --o=oname create olean file\n"; + std::cout << " -i, --i=iname create ilean file\n"; + std::cout << " -c, --c=fname name of the C output file\n"; + std::cout << " -b, --bc=fname name of the LLVM bitcode file\n"; + std::cout << " --stdin take input from stdin\n"; + std::cout << " --root=dir set package root directory from which the module name\n" + << " of the input file is calculated\n" + << " (default: current working directory)\n"; + std::cout << " -t, --trust=num trust level (default: max) 0 means do not trust any macro,\n" + << " and type check all imported modules\n"; + std::cout << " -q, --quiet do not print verbose messages\n"; + std::cout << " -M, --memory=num maximum amount of memory that should be used by Lean\n"; + std::cout << " (in megabytes)\n"; + std::cout << " -T, --timeout=num maximum number of memory allocations per task\n"; + std::cout << " this is a deterministic way of interrupting long running tasks\n"; #if defined(LEAN_MULTI_THREAD) - std::cout << " --threads=num -j number of threads used to process lean files\n"; - std::cout << " --tstack=num -s thread stack size in Kb\n"; - std::cout << " --server start lean in server mode\n"; - std::cout << " --worker start lean in server-worker mode\n"; + std::cout << " -j, --threads=num number of threads used to process lean files\n"; + std::cout << " -s, --tstack=num thread stack size in Kb\n"; + std::cout << " --server start lean in server mode\n"; + std::cout << " --worker start lean in server-worker mode\n"; #endif - std::cout << " --plugin=file load and initialize Lean shared library for registering linters etc.\n"; - std::cout << " --load-dynlib=file load shared library to make its symbols available to the interpreter\n"; - std::cout << " --json report Lean output (e.g., messages) as JSON (one per line)\n"; - std::cout << " --deps just print dependencies of a Lean input\n"; - std::cout << " --print-prefix print the installation prefix for Lean and exit\n"; - std::cout << " --print-libdir print the installation directory for Lean's built-in libraries and exit\n"; - std::cout << " --profile display elaboration/type checking time for each definition/theorem\n"; - std::cout << " --stats display environment statistics\n"; + std::cout << " --plugin=file load and initialize Lean shared library for registering linters etc.\n"; + std::cout << " --load-dynlib=file load shared library to make its symbols available to the interpreter\n"; + std::cout << " --json report Lean output (e.g., messages) as JSON (one per line)\n"; + std::cout << " --deps just print dependencies of a Lean input\n"; + std::cout << " --print-prefix print the installation prefix for Lean and exit\n"; + std::cout << " --print-libdir print the installation directory for Lean's built-in libraries and exit\n"; + std::cout << " --profile display elaboration/type checking time for each definition/theorem\n"; + std::cout << " --stats display environment statistics\n"; DEBUG_CODE( - std::cout << " --debug=tag enable assertions with the given tag\n"; + std::cout << " --debug=tag enable assertions with the given tag\n"; ) - std::cout << " -D name=value set a configuration option (see set_option command)\n"; + std::cout << " -D name=value set a configuration option (see set_option command)\n"; } static int print_prefix = 0;