search

leanprover / lean4

Lean 4 programming language and theorem prover
https://lean-lang.org
Apache License 2.0
4.69k stars 423 forks source link

`lake translate-config` does not give a helpful error message #4107

Open kim-em opened 6 months ago

kim-em commented 6 months ago

Currently lake translate-config just says: "error: missing configuration language", but should also say: Try this: lake translate-config toml (or otherwise give a clue about what to do next).

tydeu commented 6 months ago

I imagine this is a problem with other commands as well? All of them just mention the missing required argument. Perhaps Lake should print out the help page (e.g., lake translate-config --help) for the command?

kim-em commented 6 months ago

Yes, going direct to the help page would be a great solution here.