V4.25.1

[pandaman64]

Note

Migrate to Lean 4.25.1 and switch the codebase to String.Pos.Raw, updating regex/NFA semantics, strategies, iterators, utilities, tests, and proofs accordingly.

• API and types (breaking):
  • Migrate from String.Pos to String.Pos.Raw throughout: NFA.Step/Path update payloads, CaptureGroups, Strategy.Update, BoundedIterator.pos, Matches/Captures.currentPos, etc.
  • Adjust string/iterator utilities and proofs to Pos.Raw APIs; change remaining to Nat; update end/next lemmas and equality proofs.
  • Switch regex utilities to Pos.Raw.extract; remove custom HashSet helper; tweak first-chars optimization proofs.
• VM/Backtracker semantics:
  • Propagate Pos.Raw updates across ε-closure, char-step, traversal invariants, refinement, and equivalence lemmas.
• Tests:
  • Simplify parser tests (no toString roundtrip); update corpus tests to compare Pos.Raw spans.
• Tooling/Deps:
  • Upgrade Lean toolchain to v4.25.1 and bump dependencies (mathlib, doc-gen4, proofwidgets, etc.).

^{Written by Cursor Bugbot for commit fefa646. This will update automatically on new commits. Configure here.}