feat: lean --error=kind

[tydeu]

This PR adds the --error=kind option (shorthand: -Ekind) to the lean CLI. When set, messages of kind (e.g., linter.unusedVariables) will be reported as errors. This setting does nothing in interactive contexts (e.g., the server).

Closes #5194.

The spelling --error was chosen instead of the common -Werror both for practical and behavioral reasons. Behaviorally, this option effects not just warnings, but informational messages as well. Practically, -Werror conflicts with the existing -W option for the worker and lean also does not currently use long single-hyphen option names.

[digama0]

Small objection that --error=warning looks like it is making errors act like warnings and not the other way around.

[leanprover-community-bot]

Mathlib CI status (docs):

• ✅ Mathlib branch lean-pr-testing-6362 has successfully built against this PR. (2024-12-10 21:14:14) View Log
• ✅ Mathlib branch lean-pr-testing-6362 has successfully built against this PR. (2024-12-14 01:22:19) View Log

[tydeu]

@digama0

Small objection that --error=warning looks like it is making errors act like warnings and not the other way around.

Note the syntax here is --error-linter.unusedVariables. That is, it configures a specific kind to be an error, not a general category / severity (like warning). I should probably add an example to the description (EDIT: done).

[tydeu]

Separately, this could also use a test but it is not clear to me where in tests directory such a test of the lean CLI itself belong (it does not appear there are any at present). I presently just tested it manually.