declaration uses sorry bug

Stream: general

[Johan Commelin]

I have the error declaration 'foobar' uses sorry but...
I don't get any red squiggles, and I have a "Goals accomplished :tada:" at the end of my proof.
How do I debug this?

[Eric Wieser]

Does that happen if you depend on another declaration that uses sorry?

[Bryan Gin-ge Chen]

Does docs#tactic.interactive.recover do anything?

[Johan Commelin]

aha... the lemma used a definition X, and X was defined as Y quux bar sorry, where the sorry filled in some proof obligation

[Johan Commelin]

after fixing that sorry, the error/warning was gone.