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/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..a135001 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 @@ -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 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..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 @@ -323,7 +324,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..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.24.0 \ No newline at end of file +leanprover/lean4:v4.24.0