leanprover/lean4

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

Opened this issue · 2 comments

semorrison commented

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

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?

semorrison commented

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

  • 👍1