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, sincesorry
is a special concept, representing unfinished proofs, and it has special support for "go to definition", etc. - Move to ImportGraph?
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 ofsorryAx
. - sorryMsgs : Array Lean.MessageData
The uses of
sorry
that were found.
Instances For
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
.
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
#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
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
#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.