Lean server is noisy

Stream: general

[Michael Stoll]

In current Mathlib:

import Mathlib.Analysis.Complex.Basic

set_option trace.Meta.synthInstance true

#synth T2Space ℂ

in VSCode gives a pop-up window saying "Lean server printed an error: 29 79". The output window shows two lines starting with "29" and "79". Unfolding the trace in the Infoview shows lines "79 more entries..." and "29 more entries...". So it looks like the server prints out the number of additional entries when it shouldn't.

[Sebastian Ullrich]

Thanks, fixed in lean4#3622

[Ruben Van de Velde]

https://github.com/leanprover/lean4/pull/3622