Zulip Chat Archive

Stream: lean4

Topic: better formatting for `diagnostics` output


Matthew Ballard (Aug 03 2024 at 11:45):

lean#4897 makes the current output go from

info: [reduction] unfolded declarations (max: 1725, num: 4): ▼
  Nat.rec ↦ 1725
  Eq.rec ↦ 1114
  Acc.rec ↦ 1050
  PSigma.rec ↦ 513[reduction] unfolded reducible declarations (max: 1577, num: 3): ▼
  Nat.casesOn ↦ 1577
  Eq.ndrec ↦ 984
  PSigma.casesOn ↦ 513[kernel] unfolded declarations (max: 1193, num: 5): ▼
  Nat.casesOn ↦ 1193
  Nat.rec ↦ 1065
  Eq.ndrec ↦ 973
  Eq.rec ↦ 973
  Acc.rec ↦ 754use `set_option diagnostics.threshold <num>` to control threshold for reporting counters

to

info: [reduction] unfolded declarations (max: 1725, num: 4):  ▼
  [] Nat.rec ↦ 1725
  [] Eq.rec ↦ 1114
  [] Acc.rec ↦ 1050
  [] PSigma.rec ↦ 513
[reduction] unfolded reducible declarations (max: 1577, num: 3): ▼
  [] Nat.casesOn ↦ 1577
  [] Eq.ndrec ↦ 984
  [] PSigma.casesOn ↦ 513
[kernel] unfolded declarations (max: 1193, num: 5): ▼
  [] Nat.casesOn ↦ 1193
  [] Nat.rec ↦ 1065
  [] Eq.ndrec ↦ 973
  [] Eq.rec ↦ 973
  [] Acc.rec ↦ 754
use `set_option diagnostics.threshold <num>` to control threshold for reporting counters

when unfolding children in the infoview.

Per the guidelines, it is currently a draft because it has not any blessing from a developer yet.


Last updated: Feb 28 2026 at 14:05 UTC