RFC: show robust tactic state

fpvandoorn commented 2 weeks ago

Proposal

The goal of this RFC is to have the tactic state not change too much while typing. This is a complaint I have heard more than once from beginners: "The goal state is jumping around too much". You can pause the goal state, but this is a bit of an inconvenient workaround.

Examples with current behavior:

-- in each example place the pointer right before the `--`
example : True ∧ False ∧ True := by
  simp only [false_and]
  ex -- <no tactic state> / errors: unknown tactic & unsolved goals

example : True ∧ False ∧ True := by
  simp only [false_and]
  exact -- Tactic state: No goals / error: unexpected token 

example : True ∧ False ∧ True := by
  simp only [false_and]
  exact true -- Shows the correct tactic state / error: type mismatch

example : True ∧ False ∧ True := by
  simp only [false_and]
  exact true_ -- Tactic state: No goals / error: unknown identifier

example : True ∧ False ∧ True := by
  simp only [false_and]
  apply true_ -- Shows the correct tactic state / error: unknown identifier

Desired behavior: All examples should show the tactic state that is shown in examples 3 and 5.

User Experience: This should be a improvement for all users.
Beneficiaries: Especially new users, slow typers. But can benefit anyone that tries to apply a tactic, see that it errors, and wants to easily see the previous tactic state.
Maintainability: Should not significantly impact maintainability.

Implementation speculation: Hopefully the first example can be fixed by having a rule that any non-existent tactic still shows the tactic state from the start of the line. And maybe example 2 can be fixed by having a parse error do the same? Example 4 can probably be fixed in the implementation of exact (it works with apply, see example 5).

Community Feedback

Zulip

Impact

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

nomeata commented 2 weeks ago

Just crosslinking my work in that direction at https://github.com/leanprover/lean4/pull/4177.

You describe a fine goal; what I don't know though if there is going to be a simple catch-all solution, or if improved usability here is going to be a game of whack a mole where we fix different ”error conditions” one after another.

fpvandoorn commented 2 weeks ago

I expect that this will be a bit of whack-a-mole (see Implementation speculation in my first message). If it works in the 90% most common cases, that is already very helpful.

leanprover / lean4