lean[pkg build and test] should have a way to turn warnings into errors

(Apologies if this exists already, or if I'm missing how it should be done idiomatically, I looked in the below and didn't see anything else requesting this feature. Obviously if so feel free to close.)

Prerequisites

• Put an X between the brackets on this line if you have done all of the following:
  • Checked that your issue isn't already filed.
    • Specifically, check out the wishlist, open RFCs,
      or feature requests.
  • Reduced the issue to a self-contained, reproducible test case.

Description

leanpkg test should have a way to turn warnings into errors. Specifically, if I have a project and I want to fail CI if e.g. any lemmas are left using sorry, leanpkg test will exit with return code 0 (i.e. success), despite warnings being emitted to stdout. The default probably is correct, but it'd be nice to have a way to fail explicitly if any warnings are emitted.

Steps to Reproduce

printf '[package]\nname="foo"\nversion="0.1"\npath="src"\n' >leanpkg.toml && \
    mkdir src && \
    printf 'lemma foo : ∀ (x : ℕ), x = x := sorry\n' >src/foo.lean && \
    leanpkg test

Proposed behavior: [What you expect to happen]

An e.g. --warnings-as-errors flag which causes non-zero exit status due to the emitted warning.

Start with the leanpkg test command and the minimal leanpkg.toml plus src/foo.lean reproduction described in the issue. Trace how warnings are reported and how the command chooses its exit status; done means an explicit warnings-as-errors mode returns a nonzero status for the emitted sorry warning while the default behavior remains unchanged.