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?

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.

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.

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

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.

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.

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.