Return error when parse failed without exiting.

[wiio12]

This is a simple modification of the response logic when parse failed occurs.

Lean-gym currently returns a fatal error when parse fails and exits the repl process, which loses all search history. This can occur so easily, that simply inputting an empty line will can cause this issue.

I change the parse_request function that makes it return a fake LeanPEPLRequest containing the parse_failed command and error message. An additional handle_parse_failed function is also added and returns a normal error message without quitting the repl process.

I tested the change in Linux, it works fine.

p.s. great work, looking forward to future updates.

[spolu]

Looks good! Can you post an example interaction that demonstrates the returned data?

[wiio12]

Sure, I use an example from Readme. The first two is normal input examples, and the last two are the case where phase fail occurred. The last case demonstrates the cases where an empty line is entered. Hope these examples answer your questions.

["init_search", ["int.prime.dvd_mul", ""]]              
{"error":null,"proof_steps":[],"search_id":"0","tactic_state":"⊢ ∀ {m n : ℤ} {p : ℕ}, nat.prime p → ↑p ∣ m * n → p ∣ m.nat_abs ∨ p ∣ n.nat_abs","tactic_state_id":"0"}             

["run_tac",["0","0","intros"]]
{"error":null,"proof_steps":[],"search_id":"0","tactic_state":"m n : ℤ,\np : ℕ,\nhp : nat.prime p,\nh : ↑p ∣ m * n\n⊢ p ∣ m.nat_abs ∨ p ∣ n.nat_abs","tactic_state_id":"1"}

["run_tac",["0","0","in        
{"error":"parse_failed: data=[\"run_tac\",[\"0\",\"0\",\"in","proof_steps":[],"search_id":null,"tactic_state":null,"tactic_state_id":null}

{"error":"parse_failed: data=","proof_steps":[],"search_id":null,"tactic_state":null,"tactic_state_id":null}

[spolu]

LGTM