Open amit9oct opened 4 months ago
After reading the issue: https://github.com/leanprover-community/repl/issues/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.
/-- 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
I was trying to execute the following theorem via REPL:
.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 asorry
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}
.