Issues while executing tactics with ; in them.

[amit9oct]

I was trying to execute the following theorem via REPL:

theorem ftaylorSeriesWithin_univ : ftaylorSeriesWithin 𝕜 f univ = ftaylorSeries 𝕜 f := by sorry

.This theorem can be found in Mathlib in the file mathlib/Mathlib/Analysis/Calculus/ContDiff/Defs.lean (https://github.com/leanprover-community/mathlib4/blob/ae43e7f0dda4b24139e98b5033268fa1d7b09374/Mathlib/Analysis/Calculus/ContDiff/Defs.lean#L1642). I made a copy of this file by copying its contents till this theorem and replacing the proof with a sorry and removed the subsequent content of the file. I successfully loaded the theorems and definitions in this copied file via the command {"path": <path-to-copied-file> } using REPL, however, when I start running the proof line by line interactively in tactic mode via the command {'tactic': 'ext1 x; ext1 n', 'proofState': 0} (which is a valid tactic as used in the proof and works on VS Code IDE), I keep getting error: 'Lean error:\n<input>:1:6: expected end of input'. I have noticed that whenever I have ; used in the command I keep getting the same error (even in some other proofs). The error specifically points to the character ; (in this case Lean error:\n:1:6:)

Note: Everything works fine as soon as I run {'tactic': 'ext1 x', 'proofState': 0}.

[amit9oct]

After reading the issue: #25, this looks to be a similar and yet different case of the same. It seems that only linear stuff is supported in tactic mode and that is why this happens.

From code:

repl/REPL/Lean/InfoTree.lean

Line 100 in 88a0643

or is merely a tactic combinator (e.g. `by`, `;`, multiline tactics, parenthesized tactics). -/

.

/-- Decide whether a tactic is "substantive",
or is merely a tactic combinator (e.g. `by`, `;`, multiline tactics, parenthesized tactics). -/
def isSubstantive (t : TacticInfo) : Bool :=
  match t.name? with
  | none => false
  | some `null => false
  | some ``cdot => false
  | some ``cdotTk => false
  | some ``Lean.Parser.Term.byTactic => false
  | some ``Lean.Parser.Tactic.tacticSeq => false
  | some ``Lean.Parser.Tactic.tacticSeq1Indented => false
  | some ``Lean.Parser.Tactic.«tactic_<;>_» => false
  | some ``Lean.Parser.Tactic.paren => false
  | _ => true

Looks like ; gets ignore and that is why lean complains expected end of input