feat: Rust-style raw string literals

[kmill]

For example, r"\n" and r#"The word "this" is in quotes."#.

Implements #1422

[leanprover-community-mathlib4-bot]

• ❗ Mathlib CI will not be attempted unless you rebase your PR onto the 'nightly' branch. (2023-11-20 21:36:37)
• ✅ Mathlib branch lean-pr-testing-2929 has successfully built against this PR. (2023-11-28 20:27:46) View Log
• ❗ Mathlib CI can not be attempted yet, as the 'nightly-testing-2023-12-19' branch does not exist there yet. We will retry when you push more commits. It may be necessary to rebase onto 'nightly' tomorrow. (2023-12-19 17:42:28)

[hargoniX]

Is there a particular reason (apart from copying Rust syntax) that this breaks the current Lean convention of having modifiers before strings with exclamation marks (think s! and m!). I feel like it would be rather confusing for a new user that some modifiers come with ! and others with #.

[kmill]

@hargoniX One perspective here is that interpStr starts with !", and then letters are used to give what kind of interpolated string it is. Here, r plays the role of ! but for rawStr. The #'s are not playing the role of ! -- r"\n" is a raw string too.

That's just a possible interpretation of the current situation, though I think the fact we only have interpStr modifiers is worth considering. Switching from r to r! could be justifiable, if we do want to go that way.

[kmill]

@Kha I think this is ready for review

[Kha]

!bench

[leanprover-bot]

Here are the benchmark results for commit 205aa90.
There were no significant changes against commit 78200b3.

[Kha]

There is a ~1% parser run time regression. That sounds acceptable, but it might be worth a try avoiding the allocation for the rawStrLitStart result by only calling it when we're looking at an r. Makes sense?

[kmill]

@Kha I modified it to avoid allocation and to use the cheap curr == 'r' check. I also simplified the raw string parser state machine by making the states more explicit, which also saves some branching. One thing I decided is that it is OK to do lookahead for the initial ##...#" for a fast check and then parse it again to actually count the #'s, since then this fast check definitely does not need to allocate anything.

I'll run the benchmarks again once the build succeeds.

[kmill]

!bench

[tydeu]

!bench

[leanprover-bot]

Here are the benchmark results for commit 781869c.
There were no significant changes against commit 67bfa19.