feat: lake check --allow-sorry, to permit sorryAx in in-progress projects #15281

Developers of in-progress projects would like to be able to run lake check too. When we added support for nanoda to lean-action, this was requested, and supported via the nanoda-allow-sorry flag, which I would like to continue supporting when lean-action moves to lake check:

leanprover/lean-action#192 — feat: use the bundled nanoda, and deprecate the nanoda input

lake check accepts only the standard axioms and offers no way to permit sorryAx, so a single sorry anywhere in the project rejects it. That is the right default for a finished library, but it means a project still under development cannot use lake check at all, even though the bundled kernels would still be checking everything that is proved.

--allow-sorry would add sorryAx to the permitted set, and nothing else.