Turn off "declaration uses sorry"

Stream: general

[Frédéric Le Roux]

Is there a way to turn off all Lean's messages "declaration XXX uses sorry"? I am using Lean in server mode.

[Johan Commelin]

@Frédéric Le Roux see roadmap/todo.lean in the root of mathlib

[Johan Commelin]

Instead of writing sorry, you would write todo, but it would suppress all those messages.

[Frédéric Le Roux]

That seems perfect, thank you!

[Yaël Dillies]

Is it possible to do this but without having to touch the code? This looks like a feature that would belong to the infoview.