diff --git a/pyproject.toml b/pyproject.toml index 0dd65b1..2fd91f2 100644 --- a/pyproject.toml +++ b/pyproject.toml @@ -5,7 +5,7 @@ requires = [ build-backend = "hatchling.build" [project] name = "itp_interface" -version = "1.11.0" +version = "1.12.0" authors = [ { name="Amitayush Thakur", email="amitayush@utexas.edu" }, ] diff --git a/src/itp_interface/lean/tactic_parser/TacticParser.lean b/src/itp_interface/lean/tactic_parser/TacticParser.lean index 762a727..b32baf9 100644 --- a/src/itp_interface/lean/tactic_parser/TacticParser.lean +++ b/src/itp_interface/lean/tactic_parser/TacticParser.lean @@ -2,5 +2,4 @@ import TacticParser.Base64 import TacticParser.Types import TacticParser.SyntaxWalker import TacticParser.Main -import TacticParser.SyntaxWalkerMain import TacticParser.Example.simple diff --git a/src/itp_interface/lean/tactic_parser/TacticParser/DependencyParser.lean b/src/itp_interface/lean/tactic_parser/TacticParser/DependencyParser.lean index ee13796..65b86fc 100644 --- a/src/itp_interface/lean/tactic_parser/TacticParser/DependencyParser.lean +++ b/src/itp_interface/lean/tactic_parser/TacticParser/DependencyParser.lean @@ -178,7 +178,8 @@ partial def findImports (stx : Syntax) (content: String) : IO (Array ImportInfo) /-- Parse imports and namespaces from a Lean 4 file -/ def parseImports (filepath : System.FilePath) : IO DependencyInfo := do - let content ← IO.FS.readFile filepath + let mut content ← IO.FS.readFile filepath + content := if content.endsWith "\n" then content else content ++ "\n" let inputCtx := mkInputContext content filepath.toString -- Parse header which contains imports @@ -254,7 +255,10 @@ def extractConstantsFromConstInfo (cinfo : ConstantInfo) : NameSet := /-- Analyze all declarations in a file and extract their dependencies -/ unsafe def analyzeFileDependencies (filepath : System.FilePath) : IO FileDependencyAnalysis := do -- Read file content - let content ← IO.FS.readFile filepath + let mut content ← IO.FS.readFile filepath + + -- if content does not end with a newline, add one to avoid parsing issues + content := if content.endsWith "\n" then content else content ++ "\n" -- Parse basic file structure (imports and namespaces) let depInfo ← parseImports filepath diff --git a/src/itp_interface/lean/tactic_parser/TacticParser/Example/complex.lean b/src/itp_interface/lean/tactic_parser/TacticParser/Example/complex.lean index f05e8e1..4709f11 100644 --- a/src/itp_interface/lean/tactic_parser/TacticParser/Example/complex.lean +++ b/src/itp_interface/lean/tactic_parser/TacticParser/Example/complex.lean @@ -20,6 +20,4 @@ theorem additive_identity2 : simp [additive] theorem additive_comm: -∀ {a b : Nat}, addNat a b = addNat b a := by - simp [additive] - grind +∀ {a b : Nat}, addNat a b = addNat b a := by sorry \ No newline at end of file diff --git a/src/itp_interface/lean/tactic_parser/TacticParser/LineParser.lean b/src/itp_interface/lean/tactic_parser/TacticParser/LineParser.lean index 3e26b53..cc7098c 100644 --- a/src/itp_interface/lean/tactic_parser/TacticParser/LineParser.lean +++ b/src/itp_interface/lean/tactic_parser/TacticParser/LineParser.lean @@ -296,7 +296,8 @@ unsafe def parseDecls (originalContent : String) : IO (Array DeclInfo) := do /-- Parse a Lean 4 file and extract declaration information -/ unsafe def parseFile (filepath : System.FilePath) : IO (Array DeclInfo) := do - let originalContent ← IO.FS.readFile filepath + let mut originalContent ← IO.FS.readFile filepath + originalContent := if originalContent.endsWith "\n" then originalContent else originalContent ++ "\n" let (postProcessedContent, modifiedLineIdx) := postProcess originalContent let inputCtx := mkInputContext postProcessedContent filepath.toString