2024-04-01---22-10-tcg40

chore: housekeeping

2024-borrowing-baseline-NOBENCH-tag

feat: add `pp.mvars` and `pp.mvars.withType` (#3798)

* Setting `pp.mvars` to false causes metavariables to pretty print as
`?_`.
* Setting `pp.mvars.withType` to true causes metavariables to pretty
print with type ascriptions.

Motivation: when making tests, it is inconvenient using `#guard_msgs`
when there are metavariables, since the unique numbering is subject to
change.

This feature does not use `⋯` omissions since a metavariable is already
in a sense an omitted term. If repeated metavariables do not appear in
an expression, there is a chance that a term pretty printed with
`pp.mvars` set to false can still elaborate to the correct term, unlike
for other omissions.

(In the future we could consider an option that pretty prints uniquely
numbered metavariables as `?m✝`, `?m✝¹`, `?m✝²`, etc. to be able to tell
them apart, at least in the same pretty printed expression. It would
take care to make sure that these names are stable across different
hovers.)

Closes #3781

2024-borrowing-upstream-base

feat: add `pp.fieldNotation.generalized` for generalized field notati…

…on, add `@[pp_nodot]` attribute (#3737)

Refactors app delaborator, merging in the projection delaborator, to
support pretty printing with generalized field notation.

Renames option `pp.structureProjections` to `pp.fieldNotation` and adds
sub-option `pp.fieldNotation.generalized` to enable/disable generalized
field notation. Adds `@[pp_nodot]` attribute to permanently disable
using field notation for a given declaration.

For now, the default value of `pp.fieldNotation.generalized` is false
since we need a stage0 update to add `@[pp_nodot]` to some core
definitions (such as `List.toArray`) before updating the tests.

[Zulip
discussion](https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/.60pp.2EgeneralizedFieldNotation.60/near/425856054)

v4.7.0

fix: Thread unique name generator through library_search init