Iterative execution of proofs

[zhangir-azerbayev]

A common use case for the repl is writing proofs tactic by tactic. Currently, this requires re-executing the entire head of the source file. It would be great if we could iteratively execute tactic proofs. For example, I would want to be able to input

{ "cmd" : "import Mathlib.Algebra.Order.Ring.Abs\nimport Mathlib.Data.Nat.Order.Basic\nimport Mathlib.Tactic.Ring\n\nopen List\n\nexample (α : Type) (L M : List α) : (L ++ M ++ L).length = (M ++ L ++ L).length := by\n  simp\n" }

followed by

{ "cmd" : "  ring" , "env" : 0 }

Currently, the latter returns

{"sorries": [],
 "messages":
 [{"severity": "error",
   "pos": {"line": 2, "column": 2},
   "endPos": null,
   "data": "expected command"}],
 "env": 1}

[kim-em]

What have the repl remember whatever the last command was for each environment, and then have an additional instruction add or something, which just appends a line to the previous command and re-runs it?

[zhangir-azerbayev]

That is basically what I'm doing in pySagredo. However doing it this way squares runtime.

I haven't run into any scalability issues yet, so this issue isn't high priority. However, I assume I eventually will.