|
| 1 | +/- |
| 2 | +Copyright (c) 2025 Henrik Böving, Yaël Dillies, Kyle Miller. All rights reserved. |
| 3 | +Released under Apache 2.0 license as described in the file LICENSE. |
| 4 | +Authors: Henrik Böving, Yaël Dillies, Kyle Miller |
| 5 | +-/ |
| 6 | +import Mathlib.Lean.Expr.Basic |
| 7 | + |
| 8 | +/-! |
| 9 | +# Tracking uses of `sorry` |
| 10 | +
|
| 11 | +This file provides a `#print sorries` command to help find out why a given declaration is not |
| 12 | +sorry-free. `#print sorries foo` returns a non-sorry-free declaration `bar` which `foo` depends on, |
| 13 | +if such a `bar` exists. |
| 14 | +
|
| 15 | +The `#print sorries in CMD` combinator prints all sorries appearing in the declarations defined |
| 16 | +by the given command. |
| 17 | +
|
| 18 | +## TODO |
| 19 | +
|
| 20 | +* Add configuration options. `#print sorries +positions -types` would print file/line/col |
| 21 | + information and not print the types. |
| 22 | +* Make versions for other axioms/constants. |
| 23 | + The `#print sorries` command itself shouldn't be generalized, since `sorry` is a special concept, |
| 24 | + representing unfinished proofs, and it has special support for "go to definition", etc. |
| 25 | +* Move to ImportGraph? |
| 26 | +-/ |
| 27 | + |
| 28 | +open Lean Meta Elab Command |
| 29 | + |
| 30 | +namespace Mathlib.PrintSorries |
| 31 | + |
| 32 | +/-- Type of intermediate computation of sorry-tracking. -/ |
| 33 | +structure State where |
| 34 | + /-- The set of already visited declarations. -/ |
| 35 | + visited : NameSet := {} |
| 36 | + /-- The set of `sorry` expressions that have been found. |
| 37 | + Note that unlabeled sorries will only be reported in the *first* declaration that uses them, |
| 38 | + even if a later definition independently has a direct use of `sorryAx`. -/ |
| 39 | + sorries : Std.HashSet Expr := {} |
| 40 | + /-- The uses of `sorry` that were found. -/ |
| 41 | + sorryMsgs : Array MessageData := #[] |
| 42 | + |
| 43 | +/-- |
| 44 | +Collects all uses of `sorry` by the declaration `c`. |
| 45 | +It finds all transitive uses as well. |
| 46 | +
|
| 47 | +This is a version of `Lean.CollectAxioms.collect` that keeps track of enough information to print |
| 48 | +each use of `sorry`. |
| 49 | +-/ |
| 50 | +partial def collect (c : Name) : StateT State MetaM Unit := do |
| 51 | + let collectExpr (e : Expr) : StateT State MetaM Unit := do |
| 52 | + /- |
| 53 | + We assume most declarations do not contain sorry. |
| 54 | + The `getUsedConstants` function is very efficient compared to `forEachExpr'`, |
| 55 | + since `forEachExpr'` needs to instantiate fvars. |
| 56 | + Visiting constants first also guarantees that we attribute sorries to the first |
| 57 | + declaration that included it. Recall that `sorry` might appear in the type of a theorem, |
| 58 | + which leads to the `sorry` appearing directly in any declarations that use it. |
| 59 | + This is one reason we need the `State.sorries` set as well. |
| 60 | + The other reason is that we match entire sorry applications, |
| 61 | + so `forEachExpr'`'s cache won't prevent over-reporting if `sorry` is a function. |
| 62 | + -/ |
| 63 | + let consts := e.getUsedConstants |
| 64 | + consts.forM collect |
| 65 | + if consts.contains ``sorryAx then |
| 66 | + let visitSorry (e : Expr) : StateT State MetaM Unit := do |
| 67 | + unless (← get).sorries.contains e do |
| 68 | + let mut msg := m!"{.ofConstName c} has {e}" |
| 69 | + if e.isSyntheticSorry then |
| 70 | + msg := msg ++ " (from error)" |
| 71 | + try |
| 72 | + msg := msg ++ " of type" ++ indentExpr (← inferType e) |
| 73 | + catch _ => pure () |
| 74 | + msg ← addMessageContext msg |
| 75 | + modify fun s => |
| 76 | + { s with |
| 77 | + sorries := s.sorries.insert e |
| 78 | + sorryMsgs := s.sorryMsgs.push msg } |
| 79 | + Meta.forEachExpr' e fun e => do |
| 80 | + if e.isSorry then |
| 81 | + if let some _ := isLabeledSorry? e then |
| 82 | + visitSorry <| e.getBoundedAppFn (e.getAppNumArgs - 3) |
| 83 | + else |
| 84 | + visitSorry <| e.getBoundedAppFn (e.getAppNumArgs - 2) |
| 85 | + return false |
| 86 | + else |
| 87 | + -- Otherwise continue visiting subexpressions |
| 88 | + return true |
| 89 | + let s ← get |
| 90 | + unless s.visited.contains c do |
| 91 | + modify fun s => { s with visited := s.visited.insert c } |
| 92 | + let env ← getEnv |
| 93 | + match env.checked.get.find? c with |
| 94 | + | some (.axiomInfo v) => collectExpr v.type |
| 95 | + | some (.defnInfo v) => collectExpr v.type *> collectExpr v.value |
| 96 | + | some (.thmInfo v) => collectExpr v.type *> collectExpr v.value |
| 97 | + | some (.opaqueInfo v) => collectExpr v.type *> collectExpr v.value |
| 98 | + | some (.quotInfo _) => pure () |
| 99 | + | some (.ctorInfo v) => collectExpr v.type |
| 100 | + | some (.recInfo v) => collectExpr v.type |
| 101 | + | some (.inductInfo v) => collectExpr v.type *> v.ctors.forM collect |
| 102 | + | none => pure () |
| 103 | + |
| 104 | +/-- |
| 105 | +Prints all uses of `sorry` inside a list of declarations. |
| 106 | +Displayed sorries are hoverable and support "go to definition". |
| 107 | +-/ |
| 108 | +def collectSorries (constNames : Array Name) : MetaM (Array MessageData) := do |
| 109 | + let (_, s) ← (constNames.forM collect).run {} |
| 110 | + pure s.sorryMsgs |
| 111 | + |
| 112 | +/-- |
| 113 | +- `#print sorries` prints all sorries that the current module depends on. |
| 114 | +- `#print sorries id1 id2 ... idn` prints all sorries that the provided declarations depend on. |
| 115 | +- `#print sorries in CMD` prints all the sorries in declarations added by the command. |
| 116 | +
|
| 117 | +Displayed sorries are hoverable and support "go to definition". |
| 118 | +-/ |
| 119 | +syntax (name := printSorriesStx) "#print " &"sorries" (ppSpace ident)* : command |
| 120 | + |
| 121 | +/-- |
| 122 | +Collects sorries in the given constants and logs a message. |
| 123 | +-/ |
| 124 | +def evalCollectSorries (names : Array Name) : CommandElabM Unit := do |
| 125 | + let msgs ← liftTermElabM <| collectSorries names |
| 126 | + if msgs.isEmpty then |
| 127 | + logInfo m!"Declarations are sorry-free!" |
| 128 | + else |
| 129 | + logInfo <| MessageData.joinSep msgs.toList "\n" |
| 130 | + |
| 131 | +elab_rules : command |
| 132 | + | `(#print%$tk1 sorries%$tk2 $idents*) => do |
| 133 | + let mut names ← liftCoreM <| idents.flatMapM fun id => |
| 134 | + return (← realizeGlobalConstWithInfos id).toArray |
| 135 | + if names.isEmpty then |
| 136 | + names ← (← getEnv).checked.get.constants.map₂.foldlM (init := #[]) fun acc name _ => |
| 137 | + return if ← name.isBlackListed then acc else acc.push name |
| 138 | + withRef (mkNullNode #[tk1, tk2]) <| evalCollectSorries names |
| 139 | + |
| 140 | +@[inherit_doc printSorriesStx] |
| 141 | +syntax "#print " &"sorries" " in " command : command |
| 142 | + |
| 143 | +elab_rules : command |
| 144 | + | `(#print%$tk1 sorries%$tk2 in $cmd:command) => do |
| 145 | + let oldEnv ← getEnv |
| 146 | + try |
| 147 | + elabCommand cmd |
| 148 | + finally |
| 149 | + let newEnv ← getEnv |
| 150 | + let names ← newEnv.checked.get.constants.map₂.foldlM (init := #[]) fun acc name _ => do |
| 151 | + if oldEnv.constants.map₂.contains name then |
| 152 | + return acc |
| 153 | + else if ← name.isBlackListed then |
| 154 | + return acc |
| 155 | + else |
| 156 | + return acc.push name |
| 157 | + withRef (mkNullNode #[tk1, tk2]) <| evalCollectSorries names |
| 158 | + |
| 159 | +end Mathlib.PrintSorries |
0 commit comments