feat: do not propagate pretty printer errors through messages

[tydeu]

Prior to this change, pretty printer errors in messages were not uniformly handled. In core, ppExprWithInfos and ppTerm capture their errrors whereas ppGoal and ppSignature propagate them to whatever serializes the message (e.g., the frontend).

To standardize the behavior, all pretty printers in messages are now requiried to handle their errors.. That is, the signature for PPFormat now uses BaseIO. As such, ppGoal and ppSignature have been changed to capture any errors within them and print similar messages to ppExprWithInfos and ppTerm on such errors.

[leanprover-community-mathlib4-bot]

Mathlib CI status (docs):

• ❗ Std/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 0b01ceb3bb3334fd6c2f3b24996646046722c62a --onto 0ec8862103e397715854a7a6962ce542bba4884d. (2024-03-16 20:03:01)
• ❌ Mathlib branch lean-pr-testing-3696 built against this PR, but linting failed. (2024-03-26 00:03:12) View Log
• ❌ Mathlib branch lean-pr-testing-3696 built against this PR, but linting failed. (2024-03-26 00:23:32) View Log
• ❌ Mathlib branch lean-pr-testing-3696 built against this PR, but linting failed. (2024-03-26 01:31:06) View Log

[nomeata]

I guess this needs master merged into into it (or rebaesd onto master) to unblock CI. Sorry for that.

[tydeu]

Looking through the Mathlib/Std failures, there are some direct replications of ppSignature code in core which are producing errors now. To make fixing this easier, I extract this element into a separate MessageData helper ofSignature (like ofSyntax and ofExpr) that the downstream use cases can utilize. The other failures are just signature fixes and places were Mathlib/Std should now catch potential pretty-printer errors and handle them properly as well.

@semorrison Should I make PRs to the Mathlib/Std testing branches or is this something you can handle?

[kim-em]

@semorrison Should I make PRs to the Mathlib/Std testing branches or is this something you can handle?

Sorry, missed this earlier. Could you rebase onto nightly-with-mathlib (which should be quite recent), and then I can take a look.