Add proof validation to tactic mode

[augustepoiroux]

This PR introduces proof validation in tactic mode (see #44).

Highlights:

• Introduce a getProofStatus method inspired by LeanDojo validateProof method. It is called by createProofStepReponse after each tactic application.
  • Tweak introduced to achieve this: add to ProofSnapshot a rootGoals attribute (type: List MVarId) containing the initial goals of the declaration before applying any tactic.
• Add a proofStatus attribute to ProofStepResponse showing after each tactic the status of the proof up to this point.
  • Update + add new tests accordingly
• (bonus feature) Add a rootGoals attribute to CommandOption to extract initial goals and return (synthetic) sorries from each declaration in a command. It differs from allTactics in that it only extracts initial goals. Useful to test automated provers on existing Lean projects. It is similar to what LeanDojo can achieve after the tracing/parsing step.

Issues:

• Code in this PR correctly catches the apply theorem itself issue reported in [BUG] REPL accepts incorrect proofs #44 and returns an error (see test/self_proof_apply_check.in). However, it doesn't catch this issue when using the exact? tactic. From what I understand, it seems the exact? tactic should first fail at evaluation (runString method) but doesn't.
  Example:

  theorem ex : False := by
     exact?

  In Lean (and LeanDojo), it returns: `exact?\` could not close the goal. Try `apply?` to see partial suggestions.
  However, in Lean REPL in tactic mode, when we run:

  {"cmd": "theorem ex : False := sorry"}
  
  {"proofState": 0, "tactic": "exact?"}

  we get: Try this: exact _root_.ex and the tactic successfully applies.
  And I am surprised that getProofStatus doesn't catch this either. My best guess is that the proof state is decoupled from the declaration at some point. Not sure if this is indeed the case though.