instance diagnostics

Stream: lean4

[Matthew Ballard]

Can someone confirm that they get no instance stats for

set_option diagnostics true in
example : Add Nat := inferInstance

or point to what I am doing wrong?

[Matthew Ballard]

The code makes it look like it is plugged in.

[Kyle Miller]

set_option diagnostics true in
set_option diagnostics.threshold 0 in
example : Add Nat := inferInstance

[Henrik Böving]

Kyle Miller said:

set_option diagnostics true in
set_option diagnostics.threshold 0 in
example : Add Nat := inferInstance

Maybe we should implement diagnostics such that it does print a message, suggesting to set threshold lower when nothing is being printed?

[Matthew Ballard]

Is there a single threshold for all diagnostics?

[Matthew Ballard]

Matthew Ballard said:

Is there a single threshold for all diagnostics?

Yes