RFC: Show elaboration error of tactics even if a later tactic contains a parse error

Proposal

This is a follow-up of #3556. For new users it can be confusing that parse errors in tactics will prevent any elaboration errors in previous tactics from showing.

Proposal if a tactic t raises a parse error, Lean should still execute other tactics and raise their errors using the same behavior as when t would have raised an execution error.

Example:

example /- 1 -/ : False := by
  apply True.intro -- error is shown

example /- 2 -/ : False := by
  apply True.intro -- no error
  simp [

example /- 3 -/ : False := by
  apply True.intro -- no error
  sim

example /- 4 -/ : False := by
  apply True.intro -- no error
  all_goals {

example /- 5 -/  : False := by
  · apply True.intro -- error is shown
    sim

example /- 6 -/ : False ∧ False := by
  constructor
  · apply True.intro  -- error is shown
    sim
  · apply True.intro -- no error

Example 1 raises an expected error, which is not shown in examples 2-4 because of parse errors in later tactics. These tactics should also raise elaboration errors for the apply tactic.
Interestingly, when indented with ·, the elaboration error is shown (example 5).
Example 6 is trickier: if there is only an elaboration error on branch 1, branch 2 still raises elaboration errors. If there is a parse error on branch 1, branch 2 is silent.
Ideally apply True.intro raises an error in all these examples.

• User Experience: Should inform new users that their code contains errors more quickly.

Impact

Add 👍 to issues you consider important. If others benefit from the changes in this proposal being added, please ask them to add 👍 to it.

Start by reviewing the behavior described in issue #3556 and reproduce examples 1–6 from this proposal. Trace how tactic parsing and elaboration errors are handled across branches; done means earlier elaboration errors are reported even when a later tactic has a parse error.