Set `set_option pp.mvars.anonymous false` in MathlibTest?

Stream: mathlib4

[Thomas Murrills]

Should we set pp.mvars.anonymous to false in MathlibTest by default? I think we basically always want to pretty-print autogenerated mvars without their autogenerated numbers in tests for stability. :)

[Thomas Murrills]

Related (re: options used for MathlibTest): the docstring for mathlibLeanOptions in the lakefile looks stale. It reads:

/-- These options are passed as `leanOptions` to building mathlib, as well as the
`Archive` and `Counterexamples`. (`tests` omits the first two options.) -/

I'm guessing it should finish with something like "MathlibTest uses the default Lean options." instead, given that lean_lib MathlibTest does not specify any leanOptions?