Figuring out the source of `sorryAx` in a `#print axioms`

Stream: lean4

[Alex Keizer]

I'm currently looking at the result of a #print axioms foo, which I expected to be sorry-free, and am unfortunately met with the fact it does rely on sorry somewhere. So far I've just been going recursively through the theorems, and printing the axioms of all potentially suspect lemmas it uses untill I found the culprit, but this is in a fairly large project, so I wondered if there is some automated way of finding out exactly which lemma introduces the sorry?

[Leni Aniva]

you can always #eval and use a snippet to iterate over the deps of a theorem

[Julian Berman]

I think @Aaron Hill mentioned a rumor that @Yaël Dillies has something for this, a #track_sorry command, but GitHub search and Zulip search are both being poor and not showing me where it comes from.

[Bryan Gin-ge Chen]

Probably #25179? The PR description there also links to the following Zulip threads:

• #Is there code for X? > Hunting down axioms
• #Is there code for X? > ✔ Finding usages of `sorry` in external code @ 💬

[Alex Keizer]

I've found the sorry manually for now, but if this command exists, I'd love to know where it lives for next time

[Geoffrey Irving]

#track_native would also be super cool.