feat: add a stop position field to the parser

[david-christiansen]

This PR allows Lean's parser to run with a final position prior to the end of the string, so it can be invoked on a sub-region of the input.

This has applications in Verso proper, which parses Lean syntax in contexts such as code blocks and docstrings, and it is a prerequisite to parsing the contents of Lean docstrings.

[david-christiansen]

This is a draft PR for benchmarking purposes. Once everything's good to go, it can be split into two in order to use the normal infrastructure for stage0 updates.

[ghost]

Mathlib CI status (docs):

• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 890722f571c0f16a5d42c9afcab144aec6e15885 --onto 21f5263f2f28e5fd7b6a99c40f0c11351f04aedb. You can force Mathlib CI using the force-mathlib-ci label. (2025-08-22 05:11:44)

[leanprover-bot]

Reference manual CI status:

• ❗ Reference manual CI will not be attempted unless your PR branches off the nightly-with-manual branch. Try git rebase 890722f571c0f16a5d42c9afcab144aec6e15885 --onto d3dda9f6d4428a906c096067ecb75e432afc4615. You can force reference manual CI using the force-manual-ci label. (2025-08-22 05:11:45)

[david-christiansen]

!bench

[leanprover-bot]

Here are the benchmark results for commit 4ed7b9f.
There were significant changes against commit 890722f:

  Benchmark   Metric         Change
  ============================================
- parser      instructions     2.0% (1989.3 σ)

[david-christiansen]

!bench

[leanprover-bot]

Here are the benchmark results for commit c6a3eb8.
There were significant changes against commit 890722f:

  Benchmark       Metric          Change
  =================================================
+ bv_decide_mod   task-clock       -1.2%  (-71.9 σ)
+ bv_decide_mod   wall-clock       -1.2%  (-42.5 σ)
+ iterators       branch-misses    -5.0%  (-32.5 σ)
- parser          instructions      2.1% (1073.1 σ)

[david-christiansen]

That must have been a fluke...

[david-christiansen]

!bench

[leanprover-bot]

Here are the benchmark results for commit 487eed1.
There were significant changes against commit 890722f:

  Benchmark        Metric             Change
  =====================================================
+ binarytrees.st   maxrss              -7.4%  (-58.9 σ)
- parser           instructions         2.1% (1758.8 σ)
+ riscv-ast.lean   wall-clock          -1.2%  (-54.3 σ)
- stdlib           tactic execution     2.4%   (78.9 σ)
+ unionfind        maxrss              -4.7%  (-39.8 σ)