Code looks like it'll hang on multi-line tactics and statements

[JasonGross]

I haven't tried the code yet (not sure what prompts you're using), but it looks like

math-llm/interactive.py

Lines 44 to 56 in 8b3aca2

	def send(self, command: str) -> List[str]:
	"""
	Send a command to Coqtop and return its response as a list of strings.
	Args:
	command (str): The command to be sent to Coqtop.
	Returns:
	List[str]: The output from Coqtop, split into lines.
	"""
	self.child.sendline(command)
	self._expect_prompt()
	return self.child.before.decode().split("\n")

will hang if it gets something like, e.g.,

Definition f (n : nat) : nat + nat :=
  match Nat.even n with
  | true => inl (n / 2)
  | false => inr ((n - 1) / 2)
  end.

because coqtop -emacs emits no output until the end of a command. Am I reading correctly?

You might want a fancier algorithm like https://github.com/JasonGross/coq-tools/blob/49decc81e086e64984add5944efce95186fe386a/split_file.py#L135-L156

Or you can use coqc -time to get the byte ranges of statements, a la https://github.com/JasonGross/coq-tools/blob/49decc81e086e64984add5944efce95186fe386a/split_file.py#L191-L200 (just be careful of duplicate byte ranges when you have vernacular commands inside a Qed-opaque proof).