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

[fpvandoorn]

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. Thee 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.

[Kha]

RFC accepted! We should be able to reuse the infrastructure of #3556 for this but some new subtleties are bound to arise during that.