feat: set pp.mvars.anonymous false for MathlibTest

[thorimur]

This PR sets pp.mvars.anonymous false for MathlibTest in the lakefile, and removes the now-superfluous set_options which did so in individual tests.

In tests, we always want to set this option (which pretty-prints autogenerated mvars such as ?m.37 as ?_) to ensure that they are stable. Instead of looking for it during review, we can just have it always set to the correct value by default.

In fact, this PR also catches some unstable tests which slipped past during review.

It also documents the decision to not use the standard mathlib options, and removes stale documentation around mathlibLeanOptions. (Note: mathlibLeanOptions implicitly says that tests should use ⟨`maxSynthPendingDepth, .ofNat 3⟩, but we've been getting by just fine without that.)

So far this is the only option for MathlibTest, but we may as well still put it in an array to hold the documentation and not interrupt the flow of lean_libs. (And maybe make it easier set other options for MathlibTest in the future if we find we need them.)

---

I'm not sure whether this is a chore or a feat! Since it's a lakefile change I erred on the side of "feat".

[github-actions]

PR summary 34adf13417

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

---

Declarations diff (regex)

+ mathlibTestOptions

You can run this locally as follows

## from your `mathlib4` directory:
git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci

## summary with just the declaration names:
../mathlib-ci/scripts/pr_summary/declarations_diff.sh <optional_commit>

## more verbose report:
../mathlib-ci/scripts/pr_summary/declarations_diff.sh long <optional_commit>

The doc-module for scripts/pr_summary/declarations_diff.sh in the mathlib-ci repository contains some details about this script.

Declarations diff (Lean)

✅ Lean-aware diff — post-build, computed from the Lean environment (commit 34adf13).

• +0 new declarations
• −0 removed declarations

No declaration differences.

---

No changes to strong technical debt.

No changes to weak technical debt.

Current commit 34adf13417
Reference commit 17b4b96c4e

This script lives in the mathlib-ci repository. To run it locally, from your mathlib4 directory:

git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci
../mathlib-ci/scripts/reporting/technical-debt-metrics.sh pr_summary

• The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
• The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).