feat: do not propagate pretty printer errors through messages

[tydeu]

This PR makes all message constructors handle pretty printer errors.

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

To resolve this inconsistency and uniformly handle errors, the signature for ofLazy now uses BaseIO. As such, all printers been adapted 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.

[kim-em]

@tydeu, would you be able to rebase this onto nightly-with-mathlib?

[tydeu]

@kim-em I can certainly try! :-)

[leanprover-community-bot]

Mathlib CI status (docs):

• 💥 Mathlib branch lean-pr-testing-3696 build failed against this PR. (2024-12-10 05:01:36) View Log
• ✅ Mathlib branch lean-pr-testing-3696 has successfully built against this PR. (2024-12-10 10:57:25) View Log

[tydeu]

@kim-em The PR is now updated and rebased on the latest nightly-with-mathlib. i haven't investigated the Mathlib failure yet, though.

[kim-em]

Mathlib fix looks straightforward, hopefully CI will agree.

[tydeu]

@kim-em LGTM! Should I throw it on the queue?