max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

fix: diagnostics: show kernel diags even if it is the only section (#4611)

Browse source
This commit is contained in:
Joachim Breitner 2024-07-01 18:45:39 +02:00 • committed by GitHub
parent 087054172c
commit 0635b277ec
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
2 changed files with 30 additions and 11 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

25
src/Lean/Meta/Diagnostics.lean
View file

@ -69,6 +69,9 @@ def mkDiagSynthPendingFailure (failures : PHashMap Expr MessageData) : MetaM Dia
data := data.push m!"{if data.isEmpty then " " else "\n"}{msg}"
return { data }
/--
We use below that this returns `m` unchanged if `s.isEmpty`
-/
def appendSection (m : MessageData) (cls : Name) (header : String) (s : DiagSummary) (resultSummary := true) : MessageData :=
if s.isEmpty then
m
@ -86,17 +89,17 @@ def reportDiag : MetaM Unit := do
let inst ← mkDiagSummaryForUsedInstances
let synthPending ← mkDiagSynthPendingFailure (← get).diag.synthPendingFailures
let unfoldKernel ← mkDiagSummary (Kernel.getDiagnostics (← getEnv)).unfoldCounter
unless unfoldDefault.isEmpty && unfoldInstance.isEmpty && unfoldReducible.isEmpty && heu.isEmpty && inst.isEmpty && synthPending.isEmpty do
let m := MessageData.nil
let m := appendSection m `reduction "unfolded declarations" unfoldDefault
let m := appendSection m `reduction "unfolded instances" unfoldInstance
let m := appendSection m `reduction "unfolded reducible declarations" unfoldReducible
let m := appendSection m `type_class "used instances" inst
let m := appendSection m `type_class
s!"max synth pending failures (maxSynthPendingDepth: {maxSynthPendingDepth.get (← getOptions)}), use `set_option maxSynthPendingDepth <limit>`"
synthPending (resultSummary := false)
let m := appendSection m `def_eq "heuristic for solving `f a =?= f b`" heu
let m := appendSection m `kernel "unfolded declarations" unfoldKernel
let m := MessageData.nil
let m := appendSection m `reduction "unfolded declarations" unfoldDefault
let m := appendSection m `reduction "unfolded instances" unfoldInstance
let m := appendSection m `reduction "unfolded reducible declarations" unfoldReducible
let m := appendSection m `type_class "used instances" inst
let m := appendSection m `type_class
s!"max synth pending failures (maxSynthPendingDepth: {maxSynthPendingDepth.get (← getOptions)}), use `set_option maxSynthPendingDepth <limit>`"
synthPending (resultSummary := false)
let m := appendSection m `def_eq "heuristic for solving `f a =?= f b`" heu
let m := appendSection m `kernel "unfolded declarations" unfoldKernel
unless m matches .nil do
let m := m ++ "use `set_option diagnostics.threshold <num>` to control threshold for reporting counters"
logInfo m

16
tests/lean/run/ack.lean
View file

@ -33,3 +33,19 @@ set_option diagnostics.threshold 500 in
set_option diagnostics true in
theorem ex : ack 3 2 = 29 :=
rfl
/--
info: [kernel] unfolded declarations (max: 1193, num: 4):
Nat.casesOn ↦ 1193
⏎
Nat.rec ↦ 1065
⏎
Eq.ndrec ↦ 973
Eq.rec ↦ 973use `set_option diagnostics.threshold <num>` to control threshold for reporting counters
-/
#guard_msgs in
set_option diagnostics true in
set_option diagnostics.threshold 800 in
theorem ack_3_2_eq_29 : ack 3 2 = 29 := by
rfl -- uses kernel defeq checker, so only kernel diags shown