Support Lean 4 v4.27 in tactic_parser

[ChakshuGupta13]

Closes #71.

Mechanical port of tactic_parser to Lean v4.27's new String/Position API. 39+/41- across 7 files; no Python wrapper API surface or behavior change.

What changed

File	Sites	Nature
lean-toolchain	1	v4.24.0 → v4.27.0
TacticParser/Types.lean	1	content.extract ⟨0⟩ ⟨n⟩ → String.Pos.Raw.extract content ⟨0⟩ ⟨n⟩
TacticParser/SyntaxWalker.lean	6	String.Pos → String.Pos.Raw; .extract → Pos.Raw.extract; .drop/.take/.trim wrapped in .copy where assigned to String-typed bindings
TacticParser/LineParser.lean	~20	Same .copy ripple; Array (String.Pos × Syntax) → Array (String.Pos.Raw × Syntax); (⟨n⟩ : String.Pos.Raw) annotations; endPos.byteIdx → rawEndPos.byteIdx; originalContent.extract a b → String.Pos.Raw.extract …; dotted .namespace/.theorem/.lemma/.end qualified to DeclType.… (now ambiguous); 3 #eval test lines using bare-numeral position literals removed
TacticParser/ProofExtractor.lean	5	.copy wrappers on text.take/drop
TacticParser/Main.lean	2	.copy wrappers on s.take/drop
TacticParser/DependencyParser.lean	4	content.extract → String.Pos.Raw.extract; .copy wrappers on modulePath.drop

Validation

• lake build succeeds at v4.27 with only deprecation warnings (no errors).
• lake env lean --run test_user_example.lean produces a valid FileDependencyAnalysis for both Example/simple.lean and Example/complex.lean.
• 5 Python wrapper tests passed (run via the installed package; can add as src/test/test_v427_port.py if you'd like the in-tree test):
  • parse() on a simple theorem string → 4 tactics, 0 errors
  • parse_file(complex.lean, PARSE_THEOREM) → 7 decls, 0 errors
  • parse_file(simple.lean, PARSE_DEPENDS) → valid FileDependencyAnalysis, 0 errors
  • parse_file(stub, PARSE_THEOREM, project_path=Lean4Proj) with import Mathlib → 6 decls, 0 errors
  • Content assertion: declaration names + start lines on complex.lean match source
• Additional fleet test: 20/20 stubs extracted from a v4.27 Mathlib-based project (google-deepmind/formal-conjectures) parse cleanly with 0 errors and the target theorem found by name in every case (decl counts 6–19, typical range).

Known gaps / disclosures (flagging for reviewer; happy to address)

1. Checkpoint paths not exercised. I did not test BREAK_CHCKPNT / CHKPT_TACTICS. These persist Lean.Elab.Command.State across invocations, which is the most fragile path under a toolchain upgrade. My patch only touches string manipulation, so I expect them to work — but a real test would confirm.
2. Mechanical .copy style. Each Slice-returning call is wrapped with .copy rather than propagating Slice end-to-end. Minimizes diff churn; happy to do a Slice-throughout refactor as a follow-up if you prefer.
3. Pre-existing String.mk deprecation in test_user_example.lean:22 (not in patched code; surfaces as a new warning at v4.27). Easy to fix here or in a follow-up — let me know.
4. Pre-existing byte/char conflation in get_position_from_char_pos (Types.lean:326): the charPos argument is passed as a byteIdx to String.Pos.Raw. Wrong for non-ASCII source. Present in v4.24 source too — visible in the diff neighborhood but not introduced by this patch.
5. Backward-compat range. README currently advertises 4.15.0–4.24.0; this patch was developed against v4.27 and was not back-tested on 4.15–4.24. The v4.27 String.Pos split is source-incompatible, so true cross-range support would need conditional compilation or version-specific shims. Three options I see: (a) bump min version to 4.27 (drop old range), (b) maintain v4.27 as a separate branch/tag, (c) add shims. Happy to take direction from you.

[ChakshuGupta13]

Pushed an additional commit (e0d67bf) to this branch fixing two CHKPT_TACTICS bugs in Main.lean that I hit while validating the port end-to-end via COPRA on FormalConjectures files:

1. Line-offset doubling: prev_line_num was read from newchkptState after the state was updated, so position adjustments shifted by the cumulative offset including the current chunk. First call: input ends at line 69, error reported at line 138. Fix: capture prev_line_num before the state update.

2. Dangling-attribute EOF treated as fatal: chkpt_tactics callers (e.g. _skip_to_theorem) truncate input before the target theorem, leaving a dangling @[…] attribute. Lean's "unexpected end of input; expected lemma" is by-design for this mode but the Python wrapper raises on it with fail_on_error=True. Fix: filter "unexpected end of input" errors when request type is chkpt_tactics.

Bug (1) is clearly a port artifact. Bug (2) is a CHKPT_TACTICS semantic fix that likely exists on v4.21 too — same wrapper behaviour, just less commonly hit. Folded into this PR because the v4.27 port is what surfaced it during validation. Happy to split into a separate PR if you'd prefer that hygiene.

Smoke evidence: COPRA per-cell run on erdos_1056.variants.noll_simmons now produces a [FAILED] verdict after 14.5s / 5 model queries (previously: parse-error crash in 0s, zero queries).

[amit9oct]

Hi @ChakshuGupta13 ,
Thank you for your contribution. I would just request you to check if this is backwards compatible once.

I just checked:

1. This is not backwards compatible, which means it breaks for Lean 4.24.0, so we need to fix it in a way that it works for most versions post 4.15.0.
2. The CI is breaking, so probably the compatible test projects are not working (I guess because they have not been moved to the new version, and without backwards compatibility)

[ChakshuGupta13]

@amit9oct Thanks for the review. Pushed commit 7dd8da2 with a TacticParser/Compat.lean shim that restores buildability across the README's documented range.

Approach. A custom compat_pre_v427 command-elab macro checks Lean.versionString at elab time and only elaborates its body when major.minor < 4.27. On v4.27+ the shim declarations are skipped entirely — the real core API is used. Shims provided (pre-v4.27 only):

• abbrev String.Pos.Raw : Type := String.Pos
• String.Pos.Raw.extract s b e := s.extract b e
• String.rawEndPos s := s.endPos
• String.Pos.offset (identity — old Pos was already flat)
• String.copy (identity — old String.drop/take/extract already returned String)

Wired into TacticParser/Types.lean's imports, which is transitively imported by every other module.

Verified end-to-end on three toolchains (in a fresh clone of this branch — toolchain swap + rm -rf .lake + lake build + lake env lean --run test_user_example.lean):

Toolchain	Build	test_user_example.lean
v4.21.0	OK	valid FileDependencyAnalysis
v4.24.0	OK	valid FileDependencyAnalysis
v4.27.0	OK (24 jobs)	valid output (plus pre-existing String.mk deprecation warning)

The 20-stub formal-conjectures fleet probe (my private validation) still returns 20/20 on v4.27.

Caveat: this proves lake build + test_user_example parity across the range; I didn't try to back-test the full Python wrapper suite on older Pythons. The shimmed call sites all delegate to the original String API on pre-v4.27, so I'd expect behaviour parity, but if you want a tighter check I can run a wider regression — let me know.

[ChakshuGupta13]

@amit9oct Pulled the e0d67bf CI log and the failure was Unknown constant 'String' from simple_env_lean_test.py — the test project src/data/test/lean4_proj is at v4.24.0, and my port had bumped the tactic-parser sub-project to v4.27.0, causing a cross-toolchain mismatch downstream.

Pushed commit 6efebaf reverting tactic_parser/lean-toolchain to v4.24.0 (matching lean4_proj and the README's install-lean-repl default). With the Compat shim from 7dd8da2 in place, the source compiles unchanged across the range — users who want v4.27 just bump their local toolchain file.

Re-verified in the fresh clone (toolchain swap + rm -rf .lake + lake build):

Toolchain	lake build	test_user_example.lean
v4.21.0	OK	valid FileDependencyAnalysis
v4.24.0	OK (24 jobs) — tracked default	valid output
v4.27.0	OK (24 jobs)	valid output (plus pre-existing String.mk warning)

CI is currently in action_required (fork-PR approval gate) — please approve when you have a chance so we can see the green checks.

[amit9oct]

Hi @ChakshuGupta13 ,
It looks like the changes are working. I will merge even though Python 3.14 without GIL is broken (due to other reasons, I will fix it and do another release of the package, and will update COPRA too).

Again, thank you so much for your contribution.