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: May 02 2025 at 03:31 UTC