Find which declaration uses sorry

Stream: general

[Riccardo Brasca]

If I have sorry listed in #print axioms foo, is there a way to find which declaration used in the proof of foo really uses sorry? I mean, with sorry explicitly written. I've checked by hand all the declaration used in the proof such a theorem, but I didn't found any sorry, so it must be some instance or whatever.

[Floris van Doorn]

The following should give you a path from foo to a declaration that uses sorry:

meta def tactic.get_dependents_aux (env : environment) (f : expr → bool) : name →
  bool × list name × name_map bool → tactic (bool × list name × name_map bool)
| n x@(tt, p) := pure x
| n (ff, p@(l, ns)) := match ns.find n with
  | some b := pure (b, p)
  | none := do
    d ← env.get n,
    let process (v : expr) : tactic (bool × list name × name_map bool) := (do
      v.fold (pure (ff, l, ns)) $ λ e _ r, r >>= λ p,
        if f e then pure (tt, [], p.2.2) else
        if e.is_constant then tactic.get_dependents_aux e.const_name p else pure p),
    (b, l, ns) ← process d.value,
    pure (b, if b then n::l else l, ns.insert n b)
  end

meta def tactic.get_dependents (f : expr → bool) (n : name) : tactic (list name) :=
do env ← tactic.get_env,
  (b, l, ns) ← tactic.get_dependents_aux env f n (ff, [], mk_name_map),
  pure l

meta def tactic.print_path_to_sorry (nm : name) : tactic unit :=
tactic.get_dependents (λ e, e.is_sorry.is_some) nm >>= tactic.trace

#eval tactic.print_path_to_sorry `foo

(based on this post by @Mario Carneiro)

[Patrick Massot]

If this work then it should definitely be added to mathlib. This is a very useful tool for large projects.

[Floris van Doorn]

It works on sphere_eversion :-) I'll open a PR.

[Riccardo Brasca]

Thanks! I ended up doing it by hand, but I agree it's very useful.

[Floris van Doorn]

#16911

[Martin Dvořák]

In which situation is #print_sorry_in supposed to print the same lemma more than once?

[Floris van Doorn]

Never. But I can imagine that it does it if you depend on the lemma via two different routes. Feel free to PR a fix.

[Martin Dvořák]

Actually, it doesn't happen to me. I just misinterpreted the output because of line wraps.