From 93beedf7d3189d77e7425f8201668a5bb65dd886 Mon Sep 17 00:00:00 2001 From: ChakshuGupta13 Date: Sun, 31 May 2026 11:45:43 +0530 Subject: [PATCH 1/4] Support Lean 4 v4.27 in tactic_parser Lean v4.27 split String.Pos into two types: - String.Pos s (new): dependent on the string s, structure { offset : Pos.Raw, isValid : offset.IsValid s }. Returned by String.find, String.endPos, etc. - String.Pos.Raw (new, in Init.Prelude): flat { byteIdx : Nat }. Used by Lean.Syntax.Range, ModuleParserState.pos, Syntax.getPos?, etc. Ripple: String.drop, String.take, String.extract, String.takeWhile now return String.Slice rather than String. The deprecated aliases (String.trim, trimLeft, trimRight, dropRightWhile, takeRightWhile) still return String for backward compat. Mechanical port across 6 .lean files: - Replace String.Pos annotations with String.Pos.Raw where positions flow from Lean.Syntax APIs. - Wrap Slice-returning String.drop/take/extract/takeWhile calls in .copy where the result is assigned to a String-typed binding. - Use String.Pos.Raw.extract (positional) instead of the deprecated s.extract that now takes the dependent s.Pos. - Access .offset.byteIdx on dependent positions; use rawEndPos for the flat byte-end accessor. - Qualify dotted constructors (.namespace/.theorem/.lemma/.end -> DeclType.*) since these names are now ambiguous in v4.27 (Lsp.SymbolKind.namespace, Lsp.LineRange.end, etc.). - Annotate bare anonymous-constructor literals () as String.Pos.Raw since they now infer to the dependent String.Pos which needs a validity proof. Three #eval test lines using such literals removed. Bumps lean-toolchain to v4.27.0. Build: lake build succeeds with only deprecation warnings. Test: lake env lean --run test_user_example.lean produces valid FileDependencyAnalysis JSON for both Example/simple.lean and Example/complex.lean. --- .../TacticParser/DependencyParser.lean | 8 ++-- .../TacticParser/LineParser.lean | 46 +++++++++---------- .../lean/tactic_parser/TacticParser/Main.lean | 4 +- .../TacticParser/ProofExtractor.lean | 6 +-- .../TacticParser/SyntaxWalker.lean | 12 ++--- .../tactic_parser/TacticParser/Types.lean | 2 +- .../lean/tactic_parser/lean-toolchain | 2 +- 7 files changed, 39 insertions(+), 41 deletions(-) diff --git a/src/itp_interface/lean/tactic_parser/TacticParser/DependencyParser.lean b/src/itp_interface/lean/tactic_parser/TacticParser/DependencyParser.lean index 984aea6..ee13796 100644 --- a/src/itp_interface/lean/tactic_parser/TacticParser/DependencyParser.lean +++ b/src/itp_interface/lean/tactic_parser/TacticParser/DependencyParser.lean @@ -35,9 +35,9 @@ def filePathToModuleName (filepath : System.FilePath) : String := let modulePath := withoutExt.replace "/" "." -- Remove leading ./ if present if modulePath.startsWith ".." then - modulePath.drop 2 + (modulePath.drop 2).copy else if modulePath.startsWith "." then - modulePath.drop 1 + (modulePath.drop 1).copy else modulePath @@ -162,7 +162,7 @@ partial def findImports (stx : Syntax) (content: String) : IO (Array ImportInfo) match stx.getRange? with | some range => let moduleName := extractModuleName stx - let text := content.extract range.start range.stop + let text := String.Pos.Raw.extract content range.start range.stop let info : ImportInfo := { moduleName := moduleName startPos := range.start.byteIdx @@ -215,7 +215,7 @@ def parseImports (filepath : System.FilePath) : IO DependencyInfo := do match stx.getRange? with | some range => let namespaceName := extractModuleName stx - let text := content.extract range.start range.stop + let text := String.Pos.Raw.extract content range.start range.stop let info : NamespaceInfo := { name := namespaceName startPos := range.start.byteIdx diff --git a/src/itp_interface/lean/tactic_parser/TacticParser/LineParser.lean b/src/itp_interface/lean/tactic_parser/TacticParser/LineParser.lean index 9dc95a8..3e26b53 100644 --- a/src/itp_interface/lean/tactic_parser/TacticParser/LineParser.lean +++ b/src/itp_interface/lean/tactic_parser/TacticParser/LineParser.lean @@ -103,20 +103,20 @@ partial def trimComment (text : String) (state : Nat := 0) (depth : Nat := 0) : let newState := 0 -- Go till the end of line let endOfLine := text.find (fun c => c == '\n') - let remaining := text.drop endOfLine.byteIdx + let remaining := (text.drop endOfLine.offset.byteIdx).copy let ep := trimComment remaining newState depth - endOfLine.byteIdx + ep + endOfLine.offset.byteIdx + ep else if text.startsWith "/-" ∧ state == 0 then -- starting of a block comment let newState := 1 - let remaining := text.drop 2 + let remaining := (text.drop 2).copy let ep := trimComment remaining newState (depth + 1) ep + 2 else if text.startsWith "-/" ∧ state == 1 then -- ending of a block comment let newDepth := depth - 1 let newState := if newDepth == 0 then 0 else 1 - let remaining := text.drop 2 + let remaining := (text.drop 2).copy let ep := trimComment remaining newState newDepth ep + 2 else if text.length == 0 then @@ -127,7 +127,7 @@ partial def trimComment (text : String) (state : Nat := 0) (depth : Nat := 0) : -- not in comment and no leading spaces, stop 0 else - let remaining := text.drop 1 + let remaining := (text.drop 1).copy let ep := trimComment remaining state depth ep + 1 @@ -150,8 +150,8 @@ def postProcess (text : String) : String × List Nat := let lines := text.splitOn "\n" let processedLines := lines.mapIdx fun i line => if line.trimLeft.startsWith "lemma " then - let leadingSpaces := line.takeWhile (fun c => c == ' ' ∨ c == '\t') - let newLine := leadingSpaces ++ "theorem " ++ line.trimLeft.drop "lemma ".length + let leadingSpaces := (line.takeWhile (fun c => c == ' ' ∨ c == '\t')).copy + let newLine := leadingSpaces ++ "theorem " ++ (line.trimLeft.drop "lemma ".length).copy (newLine, lines.length) --(newLine, lines.length) else @@ -169,7 +169,7 @@ unsafe def parseCommon : IO (Array DeclInfo) := do -- First pass: parse all commands and collect their positions -- We parse the ORIGINAL content to find declaration boundaries - let mut commands : Array (String.Pos × Syntax) := #[] + let mut commands : Array (String.Pos.Raw × Syntax) := #[] let mut pstate := parserState let mut done := false @@ -207,20 +207,20 @@ unsafe def parseCommon let nextRealStart := match nextStx.getRange? with | some range => range.start | none => nextParsePos - ⟨nextRealStart.byteIdx - 1⟩ + (⟨nextRealStart.byteIdx - 1⟩ : String.Pos.Raw) else - ⟨originalContent.endPos.byteIdx⟩ + (⟨originalContent.rawEndPos.byteIdx⟩ : String.Pos.Raw) -- Extract text from ORIGINAL content - let text := originalContent.extract realStart endPos + let text := String.Pos.Raw.extract originalContent realStart endPos -- Strip comments to check if this starts with "lemma" let commentEnd := trimComment text - let docStringStr := (text.take commentEnd).trim + let docStringStr := (text.take commentEnd).copy.trim let mut docString := none if !docStringStr.isEmpty then docString := some docStringStr - let textWithoutComments := text.drop commentEnd + let textWithoutComments := (text.drop commentEnd).copy let isLemma := textWithoutComments.startsWith "lemma " -- Print the docstring and the text without comments for debugging @@ -233,9 +233,9 @@ unsafe def parseCommon if isLemma then -- If it's a lemma, preprocess it for parsing -- replace the "lemma" at the end position of the comment with "theorem" - textToParse := text.take commentEnd ++ + textToParse := (text.take commentEnd).copy ++ "theorem " ++ - textWithoutComments.drop "lemma ".length + (textWithoutComments.drop "lemma ".length).copy let declInputCtx := mkInputContext textToParse "" let (_, declParserState, _) ← parseHeader declInputCtx @@ -245,14 +245,14 @@ unsafe def parseCommon let declType := identifyDeclType declStx let name := extractDeclName declStx - if declType == .namespace then + if declType == DeclType.namespace then openNamespaces := openNamespaces.append [name] - else if declType == .end then + else if declType == DeclType.end then -- Pop the last opened namespace if any openNamespaces := openNamespaces.dropLast -- If we preprocessed it and it parsed as theorem, it's actually a lemma - let actualDeclType := if isLemma && declType == .theorem then .lemma else declType + let actualDeclType := if isLemma && declType == DeclType.theorem then DeclType.lemma else declType let namespc := if openNamespaces.isEmpty then none @@ -334,7 +334,7 @@ def printDeclInfo (info : DeclInfo) : IO Unit := do IO.println s!"[{info.declType}] {info.name}" IO.println s!" Position: {toJson info.startPos} - {toJson info.endPos}" let preview := if info.text.length > 100 then - info.text.take 50 ++ "\n ... more text ... \n" ++ info.text.drop (info.text.length - 50) + (info.text.take 50).copy ++ "\n ... more text ... \n" ++ (info.text.drop (info.text.length - 50)).copy else info.text IO.println s!" Text: {preview}" @@ -476,11 +476,9 @@ end Lean4Proj2 #eval parseDecls test_str -#eval (test_str.extract ⟨15⟩ ⟨37⟩) - -#eval (test_str.extract ⟨37⟩ ⟨58⟩) - -#eval (test_str.extract ⟨298⟩ ⟨912⟩) +-- v4.27 port: removed test cases using ⟨n⟩ numeric String.Pos literals +-- (the dependent String.Pos in v4.27 no longer accepts a single-field anonymous +-- constructor with bare numerals). Replace with `String.Pos.Raw.extract test_str (⟨15⟩ : String.Pos.Raw) (⟨37⟩ : String.Pos.Raw)` if needed. #eval get_position_from_char_pos test_str 57 -- expect line 4, column 20 diff --git a/src/itp_interface/lean/tactic_parser/TacticParser/Main.lean b/src/itp_interface/lean/tactic_parser/TacticParser/Main.lean index a6950c4..a6b58f7 100644 --- a/src/itp_interface/lean/tactic_parser/TacticParser/Main.lean +++ b/src/itp_interface/lean/tactic_parser/TacticParser/Main.lean @@ -62,8 +62,8 @@ instance : FromStr UserParseRequest where if s.length < parse_max_pad + 1 then none else - let pref := s.take parse_max_pad - let content := s.drop parse_max_pad + let pref := (s.take parse_max_pad).copy + let content := (s.drop parse_max_pad).copy match FromStr.fromStr pref with | some reqType => some { requestType := reqType, content := content } | none => none diff --git a/src/itp_interface/lean/tactic_parser/TacticParser/ProofExtractor.lean b/src/itp_interface/lean/tactic_parser/TacticParser/ProofExtractor.lean index 368e198..595f13a 100644 --- a/src/itp_interface/lean/tactic_parser/TacticParser/ProofExtractor.lean +++ b/src/itp_interface/lean/tactic_parser/TacticParser/ProofExtractor.lean @@ -97,7 +97,7 @@ unsafe def extractProofFromDecl -- Test each candidate for candidate in candidates do - let beforeDelimiter := text.take candidate.position + let beforeDelimiter := (text.take candidate.position).copy -- IO.println s!"beforeDelimiter:\n{beforeDelimiter}\n---" @@ -121,8 +121,8 @@ unsafe def extractProofFromDecl if success then -- Found valid split! -- IO.println s!"Found valid split at position {candidate.position} with delimiter {candidate.delimiterType}" - let proof := text.drop candidate.position - let thrm := text.take candidate.position + let proof := (text.drop candidate.position).copy + let thrm := (text.take candidate.position).copy return { declInfo with proof := some proof.trim , text := thrm.trim } -- else -- IO.println s!"Failed split at position {candidate.position} with delimiter {candidate.delimiterType}" diff --git a/src/itp_interface/lean/tactic_parser/TacticParser/SyntaxWalker.lean b/src/itp_interface/lean/tactic_parser/TacticParser/SyntaxWalker.lean index 5dd8d3a..c504999 100644 --- a/src/itp_interface/lean/tactic_parser/TacticParser/SyntaxWalker.lean +++ b/src/itp_interface/lean/tactic_parser/TacticParser/SyntaxWalker.lean @@ -70,9 +70,9 @@ open Lean.Elab open Lean.Parser open Lean.Syntax -/-- Convert a String.Pos to line and column numbers -/ -def posToLineColumn (input : String) (pos : String.Pos) : Position := - let lines := input.extract 0 pos |>.splitOn "\n" +/-- Convert a String.Pos.Raw to line and column numbers -/ +def posToLineColumn (input : String) (pos : String.Pos.Raw) : Position := + let lines := (String.Pos.Raw.extract input 0 pos).splitOn "\n" let line := lines.length let column := (lines.getLast!).length { line, column } @@ -94,7 +94,7 @@ partial def printInfoTree (input : String) (tree : InfoTree) (indent : Nat := 0) -- Extract actual text from source using byte positions let startByte := tacInfo.stx.getPos?.getD 0 let endByte := tacInfo.stx.getTailPos?.getD 0 - let actualText := input.extract startByte endByte |>.trim + let actualText := (String.Pos.Raw.extract input startByte endByte).trim let startPos := posToLineColumn input startByte let endPos := posToLineColumn input endByte @@ -251,8 +251,8 @@ def getTextFromPosition (input : String) (startPos : Position) (endPos : Positio "" else let relevantLines := (lines.take endPos.line).drop (startPos.line - 1) - let firstLine := relevantLines[0]!.drop startPos.column--.extract ⟨startPos.column⟩ ⟨relevantLines[0]!.length⟩ - let lastLine := relevantLines[relevantLines.length - 1]!.take endPos.column + let firstLine := (relevantLines[0]!.drop startPos.column).copy--.extract ⟨startPos.column⟩ ⟨relevantLines[0]!.length⟩ + let lastLine := (relevantLines[relevantLines.length - 1]!.take endPos.column).copy let middleLines := (relevantLines.take (relevantLines.length - 1)).drop 1 let actualLines := if relevantLines.length > 1 then [firstLine] ++ middleLines ++ [lastLine] else [firstLine] String.intercalate "\n" actualLines diff --git a/src/itp_interface/lean/tactic_parser/TacticParser/Types.lean b/src/itp_interface/lean/tactic_parser/TacticParser/Types.lean index 5dbac32..dc1ee5b 100644 --- a/src/itp_interface/lean/tactic_parser/TacticParser/Types.lean +++ b/src/itp_interface/lean/tactic_parser/TacticParser/Types.lean @@ -323,7 +323,7 @@ instance : Repr CheckpointedParseResult where reprPrec r _ := (repr r.parseResult) def get_position_from_char_pos (content : String) (charPos : Nat) : Position := - let before := content.extract ⟨0⟩ ⟨charPos⟩ + let before := String.Pos.Raw.extract content ⟨0⟩ ⟨charPos⟩ let lines := before.splitOn "\n" let lineCount := lines.length if lineCount == 0 then diff --git a/src/itp_interface/lean/tactic_parser/lean-toolchain b/src/itp_interface/lean/tactic_parser/lean-toolchain index 58ae245..5249182 100644 --- a/src/itp_interface/lean/tactic_parser/lean-toolchain +++ b/src/itp_interface/lean/tactic_parser/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:v4.24.0 \ No newline at end of file +leanprover/lean4:v4.27.0 From e0d67bf9a7d14624828941f28cdd01fa9b66d449 Mon Sep 17 00:00:00 2001 From: ChakshuGupta13 Date: Sun, 31 May 2026 16:53:28 +0530 Subject: [PATCH 2/4] Fix CHKPT_TACTICS line-doubling and dangling-EOF in Main.lean MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Two bugs surfaced when exercising CHKPT_TACTICS on real FormalConjectures files (e.g. ErdosProblems/1056.lean) via COPRA's _skip_to_theorem path. (1) Line-offset doubling The error/tree position-adjustment block read prev_line_num from newchkptState AFTER the state was updated with line_num + prev_line_num, so positions got shifted by the cumulative count INCLUDING the current chunk. On the first call this exactly doubled positions (input ends at line 69, error reported at line 138). Fix: capture prev_line_num before the checkpoint-state update. (2) Trailing-EOF treated as fatal chkpt_tactics callers (e.g. simple_lean4_sync_executor's _skip_to_theorem) intentionally truncate the input before the target theorem, leaving a dangling '@[…]' attribute. Lean responds with 'unexpected end of input; expected lemma' — by design for this mode, not a real parse error. But the Python wrapper raises on it under fail_on_error=True, which is what COPRA always passes. Fix: filter 'unexpected end of input' errors from the result when the request type is chkpt_tactics. Note: bug (2) is a CHKPT_TACTICS semantic fix, not strictly a v4.27 porting issue (same behavior likely on v4.21). Folded into this PR because the v4.27 port is what surfaced it during validation; happy to split into a separate PR if preferred. Validated: - lake build succeeds. - test_user_example.lean produces valid FileDependencyAnalysis. - Direct CHKPT_TACTICS probe on ErdosProblems/1056.lean prefix: returns 8 tactics, 0 errors, positions correct (was: 'expected lemma at line 138'). - COPRA per-cell smoke on erdos_1056.variants.noll_simmons now produces a [FAILED] verdict after 14.5s with 5 model queries (previously: parse error crash in 0s, no queries). --- .../lean/tactic_parser/TacticParser/Main.lean | 31 ++++++++++++------- 1 file changed, 20 insertions(+), 11 deletions(-) diff --git a/src/itp_interface/lean/tactic_parser/TacticParser/Main.lean b/src/itp_interface/lean/tactic_parser/TacticParser/Main.lean index a6b58f7..a135001 100644 --- a/src/itp_interface/lean/tactic_parser/TacticParser/Main.lean +++ b/src/itp_interface/lean/tactic_parser/TacticParser/Main.lean @@ -125,24 +125,23 @@ unsafe def processRequest (b64Input : String) (chkptState : Option CheckpointedP let chkpointParseResult ← parseTactics parse_request.content none cmdState result := chkpointParseResult.parseResult --IO.println s!"Parsed tactics with {result.trees.size} trees and {repr result.errors} errors." + -- Capture the cumulative line offset from PRIOR chunks BEFORE updating the + -- checkpoint state. Positions from `parseTactics` are local to the current + -- chunk (1-indexed lines), so the offset to shift them into document-global + -- coordinates is the cumulative count of lines from earlier chunks only — + -- NOT including this chunk's own lines. + let prev_line_num := + match newchkptState with + | some chkpt => chkpt.lineNum.getD 0 + | none => 0 if is_checkpoint_request then - -- Only changes if the checkpoint is to be updated + -- Update the checkpoint state to include this chunk's lines. let line_num := chkpointParseResult.lineNum.getD 0 - let prev_line_num := - match newchkptState with - | some chkpt => chkpt.lineNum.getD 0 - | none => 0 - -- Adjust line number based on previous checkpoint newchkptState := some { parseResult := chkpointParseResult.parseResult, lineNum := some (line_num + prev_line_num), chkptState := chkpointParseResult.chkptState } - -- Additionally, adjust error positions based on previous checkpoint - let prev_line_num := - match newchkptState with - | some chkpt => chkpt.lineNum.getD 0 - | none => 0 if prev_line_num > 0 then -- Adjust error line numbers let adjusted_errors := result.errors.map (fun err => @@ -170,6 +169,16 @@ unsafe def processRequest (b64Input : String) (chkptState : Option CheckpointedP adjust_tree tree ) result := { trees := adjusted_trees, errors := adjusted_errors } + -- For chkpt_tactics requests, the caller intentionally truncates the + -- input before the target theorem, so the parser invariably hits EOF + -- mid-declaration (e.g. after a trailing `@[…]` attribute that belongs + -- to the theorem to come). Drop "unexpected end of input" errors in + -- that mode so the Python wrapper's `fail_on_error=True` does not raise + -- on what is, for chkpt_tactics, an expected condition. + if is_checkpoint_request then + let filtered_errors := result.errors.filter (fun err => + !("unexpected end of input".isPrefixOf err.message)) + result := { result with errors := filtered_errors } else -- Unsupported request type let temp_result ← parseDecls parse_request.content From 7dd8da2b09fe5641d991facbfb3318ee3210347e Mon Sep 17 00:00:00 2001 From: ChakshuGupta13 Date: Sun, 31 May 2026 21:01:29 +0530 Subject: [PATCH 3/4] =?UTF-8?q?Restore=20backwards=20compatibility=20with?= =?UTF-8?q?=20Lean=20v4.15=E2=80=93v4.24?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Per maintainer review, the v4.27 port broke build on the README's documented support range (4.15.0 – 4.24.0) because the v4.27 String API spellings (String.Pos.Raw, .offset.byteIdx, rawEndPos, .copy) don't exist there. Adds TacticParser/Compat.lean: a thin shim file with version-gated declarations that introduce the v4.27 spellings as aliases on pre-v4.27 toolchains. The gating is implemented as a custom 'compat_pre_v427' command-elab macro that consults Lean.versionString at elab time and elaborates its body only when major.minor < 4.27. On v4.27+ the shim declarations are skipped entirely and 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, since old Pos was already flat) - String.copy (identity, since old String ops 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 clean clone of this branch (toolchain swap + rm -rf .lake + lake build + lake env lean --run test_user_example.lean): - v4.21.0: build OK, test produces valid FileDependencyAnalysis - v4.24.0: build OK, test produces valid FileDependencyAnalysis - v4.27.0: build OK (24 jobs), test produces valid FileDependencyAnalysis plus the pre-existing String.mk deprecation warning The 20-stub formal-conjectures validation probe (private) still returns 20/20 on v4.27. --- .../tactic_parser/TacticParser/Compat.lean | 81 +++++++++++++++++++ .../tactic_parser/TacticParser/Types.lean | 1 + 2 files changed, 82 insertions(+) create mode 100644 src/itp_interface/lean/tactic_parser/TacticParser/Compat.lean diff --git a/src/itp_interface/lean/tactic_parser/TacticParser/Compat.lean b/src/itp_interface/lean/tactic_parser/TacticParser/Compat.lean new file mode 100644 index 0000000..f78c6d0 --- /dev/null +++ b/src/itp_interface/lean/tactic_parser/TacticParser/Compat.lean @@ -0,0 +1,81 @@ +import Lean + +/-! +# Compatibility shims for Lean version skew + +In Lean v4.27, `String.Pos` was split into two types: + + * `String.Pos s` (new, dependent): `{ offset : Pos.Raw, isValid : offset.IsValid s }` + * `String.Pos.Raw` (new, flat): `{ byteIdx : Nat }` — the old `String.Pos` + +Several `String` operations also changed return type: + + * `String.drop`, `String.take`, `String.extract`, `String.takeWhile`, etc. + now return `String.Slice` (which has a `.copy : String.Slice → String`). + Pre-v4.27 they returned `String` directly. + +The `TacticParser` source uses the v4.27 spellings (`String.Pos.Raw.extract`, +`.offset.byteIdx`, `.copy`, `rawEndPos`). To stay buildable on the README's +documented range (4.15.0 – 4.24.0) as well as v4.27.0, this file provides +shims that are elaborated *only* on pre-v4.27 toolchains; on v4.27+ they are +skipped, so the real core definitions are used. + +The `compat_pre_v427` macro is a tiny preprocessor that runs its body iff +`Lean.versionString` parses to `< 4.27`. +-/ + +open Lean Elab Command + +/-- True iff the current Lean toolchain is older than v4.27. -/ +private def itpInterface_isPreV427 : Bool := Id.run do + let parts := Lean.versionString.splitOn "." + let some majorStr := parts.head? | return false + let some minorStr := parts[1]? | return false + let some major := majorStr.toNat? | return false + -- Strip any suffix like "-rc1" before parsing minor. + let minorClean := minorStr.takeWhile Char.isDigit + let some minor := minorClean.toNat? | return false + return major < 4 || (major == 4 && minor < 27) + +/-- Elaborate the body iff the current Lean toolchain is older than v4.27. -/ +syntax (name := compatPreV427) "compat_pre_v427 " command* : command + +@[command_elab compatPreV427] +def elabCompatPreV427 : CommandElab := fun stx => do + if itpInterface_isPreV427 then + let cmds := stx[1].getArgs + for c in cmds do + elabCommand c + +-- --------------------------------------------------------------------------- +-- Pre-v4.27 shims. +-- +-- On v4.27 these are NOT elaborated; the real core definitions are used. +-- On v4.15–4.24 these introduce the v4.27 spellings as thin wrappers. +-- --------------------------------------------------------------------------- + +compat_pre_v427 + /-- Pre-v4.27 alias: the (then-flat) `String.Pos` plays the role of the new + `String.Pos.Raw`. -/ + abbrev String.Pos.Raw : Type := String.Pos + + namespace String.Pos.Raw + /-- Pre-v4.27 shim mirroring the v4.27 positional spelling + `String.Pos.Raw.extract s b e`. -/ + def extract (s : String) (b e : String.Pos) : String := s.extract b e + end String.Pos.Raw + + /-- Pre-v4.27 shim: in v4.27 a `String` exposes a flat past-the-end accessor + `rawEndPos : Pos.Raw`. Pre-v4.27 only has `endPos`. -/ + def String.rawEndPos (s : String) : String.Pos := s.endPos + + namespace String.Pos + /-- Pre-v4.27 shim: in v4.27 a dependent `String.Pos s` carries a `.offset : Pos.Raw` + field. Pre-v4.27 the position is already flat, so `.offset` is the identity. -/ + def offset (p : String.Pos) : String.Pos := p + end String.Pos + + /-- Pre-v4.27 shim: in v4.27 `String.drop`/`take`/`extract`/`takeWhile` return + `String.Slice` and call sites use `.copy` to materialise back to `String`. + Pre-v4.27 they already return `String`, so `.copy` is the identity. -/ + def String.copy (s : String) : String := s diff --git a/src/itp_interface/lean/tactic_parser/TacticParser/Types.lean b/src/itp_interface/lean/tactic_parser/TacticParser/Types.lean index dc1ee5b..b648db5 100644 --- a/src/itp_interface/lean/tactic_parser/TacticParser/Types.lean +++ b/src/itp_interface/lean/tactic_parser/TacticParser/Types.lean @@ -3,6 +3,7 @@ Types for tactic information. -/ import Lean import Lean.Elab.Frontend +import TacticParser.Compat namespace TacticParser From 6efebaf75ffbf077f95696e8eb49f6a17e623c02 Mon Sep 17 00:00:00 2001 From: ChakshuGupta13 Date: Sun, 31 May 2026 21:07:49 +0530 Subject: [PATCH 4/4] Revert lean-toolchain default to v4.24.0 (CI alignment) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Per @amit9oct's CI run on e0d67bf, the CI test project src/data/test/lean4_proj uses lean-toolchain v4.24.0, but my port had bumped the tactic-parser sub-project's lean-toolchain to v4.27.0. That mismatch caused the downstream parser tests to fail with 'Unknown constant String' when the v4.27-built parser tried to parse v4.24-built lean4_proj sources. Now that TacticParser/Compat.lean (commit 7dd8da2) makes the source buildable across the v4.15–v4.27 range, the tracked lean-toolchain can stay at v4.24.0 (matching lean4_proj and the install-lean-repl default per README), and users who want v4.27 just bump their local lean-toolchain file — the source compiles unchanged. Re-verified on three toolchains in a fresh clone (toolchain swap + rm -rf .lake + lake build): - v4.21.0: Build completed successfully - v4.24.0: Build completed successfully (24 jobs) [tracked default] - v4.27.0: Build completed successfully (24 jobs) test_user_example.lean produces valid FileDependencyAnalysis on all three. --- src/itp_interface/lean/tactic_parser/lean-toolchain | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/itp_interface/lean/tactic_parser/lean-toolchain b/src/itp_interface/lean/tactic_parser/lean-toolchain index 5249182..c00a535 100644 --- a/src/itp_interface/lean/tactic_parser/lean-toolchain +++ b/src/itp_interface/lean/tactic_parser/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:v4.27.0 +leanprover/lean4:v4.24.0