semicolon and tactic state display

[bryangingechen]

I wish we could see how the tactic state changes before and after semicolons.

I asked Mario about this in this Zulip thread: https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/semicolon.20and.20tactic.20state

Apparently this requires changes to the global parser?

[bryangingechen]

Is it possible to display not just the first goal, but all goals?

example : true ∧ true ∧ true := 
by split; split; trivial
       -- ^ 1 goal:\n⊢ true
/- but I'd rather see: 2 goals:\n⊢ true\n⊢ true ∧ true -/
              -- ^ 1 goal:\n⊢ true
/- but I'd rather see: 2 goals:\n⊢ true\n⊢ true -/

[digama0]

The problem is that your gloss is not true - there are not 2 goals after the first tactic, there is one goal and the second tactic is read twice. The wording 1 goal and a list corresponds to the printing of get_goals at that point, and it is correct.

What I would rather see is

example : true ∧ true ∧ true := 
by split; split; trivial
       -- ^ 1 goal:\n⊢ true
/- but I'd rather see: 
1 goal:
⊢ true

1 goal:
⊢ true ∧ true -/

where the two responses mean that lean has responded twice to a get_goal_state query from vscode.

[digama0]

The advantage of this approach is that you can more easily follow what happens in complex tactic blocks that are being evaluated multiple times by all_goals, ; and so on. Every time execution passes by a certain point lean triggers another goal state report, so if you have a complicated parallel proof you can see progress in all branches rather than just the first. This is an entirely separate concept from multiple goals and it would be a good idea not to visually mix them.

[bryangingechen]

Thanks Mario, that makes better sense.

[fpvandoorn]

A related bug report (possibly caused by #239?):

In the following example, the tactic before any tactic involving ; shows only 1 goal instead of all the goals

import order.lattice

variables {α : Type*} [lattice α] {x y z : α}
example : (x ⊓ y) ⊓ z = x ⊓ (y ⊓ z) :=
begin
    apply le_antisymm, -- cursor here shows 1 goal
    apply le_inf; sorry,
end