Skip to content

Commit 2d09c96

Browse files
authored
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).
1 parent 21b4377 commit 2d09c96

File tree

1 file changed

+34
-33
lines changed

1 file changed

+34
-33
lines changed

src/util/shell.cpp

Lines changed: 34 additions & 33 deletions
Original file line numberDiff line numberDiff line change
@@ -191,43 +191,44 @@ static void display_features(std::ostream & out) {
191191
static void display_help(std::ostream & out) {
192192
display_header(out);
193193
std::cout << "Miscellaneous:\n";
194-
std::cout << " --help -h display this message\n";
195-
std::cout << " --features -f display features compiler provides (eg. LLVM support)\n";
196-
std::cout << " --version -v display version number\n";
197-
std::cout << " --githash display the git commit hash number used to build this binary\n";
198-
std::cout << " --run call the 'main' definition in a file with the remaining arguments\n";
199-
std::cout << " --o=oname -o create olean file\n";
200-
std::cout << " --i=iname -i create ilean file\n";
201-
std::cout << " --c=fname -c name of the C output file\n";
202-
std::cout << " --bc=fname -b name of the LLVM bitcode file\n";
203-
std::cout << " --stdin take input from stdin\n";
204-
std::cout << " --root=dir set package root directory from which the module name of the input file is calculated\n"
205-
<< " (default: current working directory)\n";
206-
std::cout << " --trust=num -t trust level (default: max) 0 means do not trust any macro,\n"
207-
<< " and type check all imported modules\n";
208-
std::cout << " --quiet -q do not print verbose messages\n";
209-
std::cout << " --memory=num -M maximum amount of memory that should be used by Lean\n";
210-
std::cout << " (in megabytes)\n";
211-
std::cout << " --timeout=num -T maximum number of memory allocations per task\n";
212-
std::cout << " this is a deterministic way of interrupting long running tasks\n";
194+
std::cout << " -h, --help display this message\n";
195+
std::cout << " -f, --features display features compiler provides (eg. LLVM support)\n";
196+
std::cout << " -v, --version display version number\n";
197+
std::cout << " --githash display the git commit hash number used to build this binary\n";
198+
std::cout << " --run call the 'main' definition in a file with the remaining arguments\n";
199+
std::cout << " -o, --o=oname create olean file\n";
200+
std::cout << " -i, --i=iname create ilean file\n";
201+
std::cout << " -c, --c=fname name of the C output file\n";
202+
std::cout << " -b, --bc=fname name of the LLVM bitcode file\n";
203+
std::cout << " --stdin take input from stdin\n";
204+
std::cout << " --root=dir set package root directory from which the module name\n"
205+
<< " of the input file is calculated\n"
206+
<< " (default: current working directory)\n";
207+
std::cout << " -t, --trust=num trust level (default: max) 0 means do not trust any macro,\n"
208+
<< " and type check all imported modules\n";
209+
std::cout << " -q, --quiet do not print verbose messages\n";
210+
std::cout << " -M, --memory=num maximum amount of memory that should be used by Lean\n";
211+
std::cout << " (in megabytes)\n";
212+
std::cout << " -T, --timeout=num maximum number of memory allocations per task\n";
213+
std::cout << " this is a deterministic way of interrupting long running tasks\n";
213214
#if defined(LEAN_MULTI_THREAD)
214-
std::cout << " --threads=num -j number of threads used to process lean files\n";
215-
std::cout << " --tstack=num -s thread stack size in Kb\n";
216-
std::cout << " --server start lean in server mode\n";
217-
std::cout << " --worker start lean in server-worker mode\n";
215+
std::cout << " -j, --threads=num number of threads used to process lean files\n";
216+
std::cout << " -s, --tstack=num thread stack size in Kb\n";
217+
std::cout << " --server start lean in server mode\n";
218+
std::cout << " --worker start lean in server-worker mode\n";
218219
#endif
219-
std::cout << " --plugin=file load and initialize Lean shared library for registering linters etc.\n";
220-
std::cout << " --load-dynlib=file load shared library to make its symbols available to the interpreter\n";
221-
std::cout << " --json report Lean output (e.g., messages) as JSON (one per line)\n";
222-
std::cout << " --deps just print dependencies of a Lean input\n";
223-
std::cout << " --print-prefix print the installation prefix for Lean and exit\n";
224-
std::cout << " --print-libdir print the installation directory for Lean's built-in libraries and exit\n";
225-
std::cout << " --profile display elaboration/type checking time for each definition/theorem\n";
226-
std::cout << " --stats display environment statistics\n";
220+
std::cout << " --plugin=file load and initialize Lean shared library for registering linters etc.\n";
221+
std::cout << " --load-dynlib=file load shared library to make its symbols available to the interpreter\n";
222+
std::cout << " --json report Lean output (e.g., messages) as JSON (one per line)\n";
223+
std::cout << " --deps just print dependencies of a Lean input\n";
224+
std::cout << " --print-prefix print the installation prefix for Lean and exit\n";
225+
std::cout << " --print-libdir print the installation directory for Lean's built-in libraries and exit\n";
226+
std::cout << " --profile display elaboration/type checking time for each definition/theorem\n";
227+
std::cout << " --stats display environment statistics\n";
227228
DEBUG_CODE(
228-
std::cout << " --debug=tag enable assertions with the given tag\n";
229+
std::cout << " --debug=tag enable assertions with the given tag\n";
229230
)
230-
std::cout << " -D name=value set a configuration option (see set_option command)\n";
231+
std::cout << " -D name=value set a configuration option (see set_option command)\n";
231232
}
232233

233234
static int print_prefix = 0;

0 commit comments

Comments
 (0)