Check "this theorem/instantinate has no sorry!" in CI

Stream: general

[SnO2WMaN]

I know to use #print axioms for checking that proof doesn't depend sorryAx manually.

However, is there some way (to add an annotation?) to check "this theorem does not depend on sorry" and if does, print warning (local) or build failed (in CI)? In our project, I use lake -K -Kenv=ci build, so changing behavior seemed to be easy...

[Johan Commelin]

This may help: https://leanprover.zulipchat.com/#narrow/stream/348111-batteries/topic/scope.20of.20std/near/412282298