Commit 2025-08-29 02:42 e81e752a

feat: #print sorries, a command to find usage of sorry (#25179) Adds the #print sorries command. Without arguments, prints all sorries used by all declarations in the current file. #print sorries id1 ... idn prints all sorries by declarations id1, ..., idn. If the sorry has source position information, it supports "go to definition" to see exactly where in the source code it was introduced. For convenience, the types of the sorries are pretty printed as well. This also gives #print sorries in (like whatsnew in) to print all sorries used by the following declaration. The needs from a #print sorries command are different from #print axioms. Users add sorry as a placeholder for unfinished work, and the elaborator adds sorry to replace erroneous work. The fact that sorry is an axiom is an implementation detail. The command serves the need of finding what should be worked on next. Such a command is a recurrent need of the community, see eg here on Zulip. This PR combines code from toric and code written at the ICERM "Autoformalization for the Working Mathematician" workshop.