feat: custom error recovery in parser

[david-christiansen]

Adds a simple error-recovery mechanism to Lean's parser, similar to those used in other combinator parsing libraries.

Lean itself isn't very amenable to error recovery with this mechanism, as it requires global knowledge of the grammar in question to write recovery rules that don't break backtracking or <|>. I only found a few opportunities.

But for DSLs, this is really important. In particular, Verso parse errors interacted very badly with Lean parse errors in a way that required frequent "restart file" commands, but this mechanism allows me to both recover from Verso parse errors and to have Lean skip the rest of the file rather than repeatedly trying to parse it as Lean commands.

[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. (2024-02-20 10:27:00)
• ✅ Mathlib branch lean-pr-testing-3413 has successfully built against this PR. (2024-02-20 13:36:13) View Log
• 🟡 Mathlib branch lean-pr-testing-3413 build against this PR was cancelled. (2024-02-20 14:56:44) View Log
• ✅ Mathlib branch lean-pr-testing-3413 has successfully built against this PR. (2024-02-20 17:16:04) View Log

[david-christiansen]

!bench

[leanprover-bot]

Here are the benchmark results for commit 253dda4.
There were no significant changes against commit 0e0ed9c.

[Kha]

The parser framework changes look great. For the grammar changes it would be nice to have a less manual approach as discussed but this is a good start.