# Tracking uses of `sorry` #

This file provides a `#print sorries` command to help find out why a given declaration is not sorry-free. `#print sorries foo` returns a non-sorry-free declaration `bar` which `foo` depends on, if such a `bar` exists.

The `#print sorries in CMD` combinator prints all sorries appearing in the declarations defined by the given command.

## TODO #

- Add configuration options. `#print sorries +positions -types` would print file/line/col information and not print the types.
- Make versions for other axioms/constants. The `#print sorries` command itself shouldn't be generalized, since `sorry` is a special concept, representing unfinished proofs, and it has special support for "go to definition", etc.
- Move to ImportGraph?

source
structure Mathlib.PrintSorries.State :
Type

Type of intermediate computation of sorry-tracking.

- visited : Lean.NameSet

  The set of already visited declarations.

- sorries : Std.HashSet Lean.Expr

  The set of `sorry` expressions that have been found. Note that unlabeled sorries will only be reported in the first declaration that uses them, even if a later definition independently has a direct use of `sorryAx`.

- sorryMsgs : Array Lean.MessageData

  The uses of `sorry` that were found.

Instances For

source
partial def Mathlib.PrintSorries.collect (c : Lean.Name) :
StateT State Lean.MetaM Unit

Collects all uses of `sorry` by the declaration `c`. It finds all transitive uses as well.

This is a version of `Lean.CollectAxioms.collect` that keeps track of enough information to print each use of `sorry`.

source
def Mathlib.PrintSorries.collectSorries (constNames : Array Lean.Name) :
Lean.MetaM (Array Lean.MessageData)

Prints all uses of `sorry` inside a list of declarations. Displayed sorries are hoverable and support "go to definition".

Equations

- Mathlib.PrintSorries.collectSorries constNames = do let __discr ← (Array.forM Mathlib.PrintSorries.collect constNames).run { } match __discr with | (fst, s) => pure s.sorryMsgs

Instances For

source
def Mathlib.PrintSorries.printSorriesStx :
Lean.ParserDescr

- `#print sorries` prints all sorries that the current module depends on.
- `#print sorries id1 id2 ... idn` prints all sorries that the provided declarations depend on.
- `#print sorries in CMD` prints all the sorries in declarations added by the command.

Displayed sorries are hoverable and support "go to definition".

Equations

- One or more equations did not get rendered due to their size.

Instances For

source
def Mathlib.PrintSorries.evalCollectSorries (names : Array Lean.Name) :
Lean.Elab.Command.CommandElabM Unit

Collects sorries in the given constants and logs a message.

Equations

- One or more equations did not get rendered due to their size.

Instances For

source
def Mathlib.PrintSorries.«command#printSorriesIn_» :
Lean.ParserDescr

- `#print sorries` prints all sorries that the current module depends on.
- `#print sorries id1 id2 ... idn` prints all sorries that the provided declarations depend on.
- `#print sorries in CMD` prints all the sorries in declarations added by the command.

Displayed sorries are hoverable and support "go to definition".

Equations

- One or more equations did not get rendered due to their size.

Instances For