## Stream: lean4

### Topic: goal view

#### Reid Barton (Jan 11 2021 at 15:12):

There's no goal view yet right?

#### Kenny Lau (Jan 11 2021 at 15:21):

there is the problems panel on the bottom

#### Adam Topaz (Jan 11 2021 at 15:22):

In emacs the "next error" window works.

#### Reid Barton (Jan 11 2021 at 15:27):

But there's no way to see the tactic state at positions where there wasn't an error?

#### Reid Barton (Jan 11 2021 at 15:27):

I guess "make an error happen" works

#### Reid Barton (Jan 11 2021 at 19:02):

(A good way to do this is to use the done tactic)

#### Julian Berman (Jan 11 2021 at 19:21):

I think the implementation of this relies on hover support (which was mentioned isn't there yet) -- I don't see the goal state either, just diagnostics

#### Sebastian Ullrich (Mar 30 2021 at 21:12):

In some ways, the comma was the most important token in a Lean 3 proof: everyone quickly learned to place their cursor on it whenever they wanted to see the goal resulting from execution of a tactic. Now you might know that Lean 4 does away with the comma, preferring tactic separation by whitespace instead. Which begs the question: which goal state should we display where?
The simple solution is to still show the new state resulting from a tactic only strictly after it - even if there is no comma, you can place your cursor at the end of the line (except when you're in vim normal mode, oh well). However, I wanted to take the disappearance of the comma as an opportunity to advocate for showing the resulting state when located anywhere on the tactic instead: when I'm working on a tactic, e.g. refining the set of lemmas passed to simp, I really want to see the resulting state without having to move my cursor. All the same information as before is still accessible, it's just shifted - in the case of the initial state of a tactic block, it should be shifted onto the initial token such as by.

To illustrate the two approaches, using | to show where the tactic state changes:

by
intro h|
apply h|


My proposal:

by
|intro h
|apply h


There has been some pushback against this idea :), so I would like to hear what behavior the community feels more intuitive and helpful (and not just familiar from Lean 3), but also in particular if you seen any specific UX issues in either of the approaches that the other one solves.

#### Yakov Pechersky (Mar 30 2021 at 21:14):

What happens with rw [lemma1, lemma2, lemma3] blocks? Currently, one can scrub through the commas to see the effect of each cumulative rewrite.

#### Patrick Massot (Mar 30 2021 at 21:15):

The first one certainly feels more intuitive. The tactic changes the proof state, hence I expect to see the new proof state after the tactic.

#### Yakov Pechersky (Mar 30 2021 at 21:16):

Semantically -- cursor on top of the rw shows the state after 0, 1, or all of the rewrites?

#### Sebastian Ullrich (Mar 30 2021 at 21:19):

Zulip first duplicated, then deleted my message, oops. But rw would be shifted the same way - rw [|lemma1, |lemma2, |lemma3].

#### Sebastian Ullrich (Mar 30 2021 at 21:20):

Another solution could be to more fundamentally change how the UI works - users could select whether to show the state before or after execution, or even a fancy diff of them. But I think there still should be a sensible default choice presented first.

#### Mario Carneiro (Mar 30 2021 at 21:21):

What about changing after the first character? i.e i|ntro h in your notation

#### Mario Carneiro (Mar 30 2021 at 21:22):

I think if you have the cursor at the beginning of the line, then this should be "before the tactic", but if you are any point after that then you are after the tactic

#### Mario Carneiro (Mar 30 2021 at 21:23):

This is useful when you are in the middle of writing the tactic application; in lean 3 you have to make your edit and then move the cursor to the end to see if the change had the desired effect (for example, when adding lemmas to a simp only call)

#### Daniel Fabian (Mar 30 2021 at 21:24):

for completeness, I'd like to also offer this option: intro |h and simp [A|, B|, C|]. This fixes the vim normal mode issue to a certain point.

#### Sebastian Ullrich (Mar 30 2021 at 21:25):

@Mario Carneiro Interesting. At first it looks wrong to just hack apart the word "intro" like that, but as you said, being on the first character really means being in front of the tactic with the usual cursor semantics.

#### Mario Carneiro (Mar 30 2021 at 21:25):

The fact that it looks like I'm hacking apart the word is only a side effect of the semantics you applied to the |. I'm switching < and <=

#### Julian Berman (Mar 30 2021 at 21:26):

(For the vim normal mode one, which I guess I care about... we're using | but the cursor is generally always at a particular character, so I guess to me are we saying the position after the last h then? i.e. the newline character itself? Not on the h?) Also maybe relatedly I'd love a way to iterate over the points at which the tactic state changes, but maybe that's a separate thing.

#### Mario Carneiro (Mar 30 2021 at 21:26):

That is, if the tactic has span start..end then you see the before if you are at cursor <= start

#### Mario Carneiro (Mar 30 2021 at 21:28):

For intro |h and things: The ability to support intra tactic states is something that is specific to the tactic itself. Any tactic could implement this, but in lean 3 only rw does

#### Mario Carneiro (Mar 30 2021 at 21:30):

You have to write the tactic in a certain way, such that intermediate states both (1) actually correspond to a moment in the middle of execution and (2) can be mapped to spans in the expression provided by the user. For most tactics this just doesn't make sense - for example in simp [A, B, C], there is no moment when you have just A and B applied, because they can be applied in any order and as many times as necessary

#### Sebastian Ullrich (Mar 30 2021 at 21:30):

Another issue/question is duplication with error messages - when I'm working on a tactic, even if it displays the "pre state", I still usually see the "post state" in the "unsolved goals" message below - except when the pre state is so big that I would have to fold it first. Not sure if there is any fundamentally nicer way to present all this information.

#### Mario Carneiro (Mar 30 2021 at 21:33):

Another issue with error messages is that It is often hard to find the relevant information. For example, here's a random error message from a proof I'm working on now:

Tactic state:
4 goals
BD : data,
c' : ℕ → ℝ≥0,
_inst_1 : BD.suitable c',
r : ℝ≥0,
V : NormedGroup,
_inst_4 : normed_with_aut ↑r V,
_inst_5 : fact (0 < r),
r' : ℝ≥0,
_inst_6 : fact (0 < r'),
_inst_7 : fact (r' ≤ 1),
M : ProFiltPseuNormGrpWithTinv r',
c N : ℝ≥0
⊢ bar BD r V M (λ (i : ℕ), r' * (c * (c' i * N⁻¹))) (λ (i : ℕ), c * (c' i * N⁻¹)) ?m_1 ?m_2 _ _ = ?m_3

BD : data,
c' : ℕ → ℝ≥0,
_inst_1 : BD.suitable c',
r : ℝ≥0,
V : NormedGroup,
_inst_4 : normed_with_aut ↑r V,
_inst_5 : fact (0 < r),
r' : ℝ≥0,
_inst_6 : fact (0 < r'),
_inst_7 : fact (r' ≤ 1),
M : ProFiltPseuNormGrpWithTinv r',
c N : ℝ≥0
⊢ ∀ (i j : ℕ), universal_map.suitable (r' * (c * (c' j * N⁻¹))) (r' * (c * (c' i * N⁻¹))) (BD.d j i)

BD : data,
c' : ℕ → ℝ≥0,
_inst_1 : BD.suitable c',
r : ℝ≥0,
V : NormedGroup,
_inst_4 : normed_with_aut ↑r V,
_inst_5 : fact (0 < r),
r' : ℝ≥0,
_inst_6 : fact (0 < r'),
_inst_7 : fact (r' ≤ 1),
M : ProFiltPseuNormGrpWithTinv r',
c N : ℝ≥0
⊢ ∀ (i j : ℕ), universal_map.suitable (c * (c' j * N⁻¹)) (c * (c' i * N⁻¹)) (BD.d j i)

BD : data,
c' : ℕ → ℝ≥0,
_inst_1 : BD.suitable c',
r : ℝ≥0,
V : NormedGroup,
_inst_4 : normed_with_aut ↑r V,
_inst_5 : fact (0 < r),
r' : ℝ≥0,
_inst_6 : fact (0 < r'),
_inst_7 : fact (r' ≤ 1),
M : ProFiltPseuNormGrpWithTinv r',
c N : ℝ≥0
⊢ ?m_1 =
cochain_complex.mk
(λ (i : ℕ),
(BD.complex₂_X r V r' (λ (i : ℕ), c * c' i) (λ (i : ℕ), r' * (c * c' i)) i).obj
(opposite.op (of r' (rescale N ↥M))))
(λ (i j : ℕ),
(universal_map.eval_CLCFPTinv₂ r V r' (c * c' i) (r' * (c * c' i)) (c * c' j) (r' * (c * c' j))
(BD.d j i)).app
(opposite.op (of r' (rescale N ↥M))))
_
_

homotopy.lean:165:2
simplify tactic failed to simplify
state:
4 goals
BD : data,
c' : ℕ → ℝ≥0,
_inst_1 : BD.suitable c',
r : ℝ≥0,
V : NormedGroup,
_inst_4 : normed_with_aut ↑r V,
_inst_5 : fact (0 < r),
r' : ℝ≥0,
_inst_6 : fact (0 < r'),
_inst_7 : fact (r' ≤ 1),
M : ProFiltPseuNormGrpWithTinv r',
c N : ℝ≥0
⊢ bar BD r V M (λ (i : ℕ), r' * (c * (c' i * N⁻¹))) (λ (i : ℕ), c * (c' i * N⁻¹)) ?m_1 ?m_2 _ _ = ?m_3

BD : data,
c' : ℕ → ℝ≥0,
_inst_1 : BD.suitable c',
r : ℝ≥0,
V : NormedGroup,
_inst_4 : normed_with_aut ↑r V,
_inst_5 : fact (0 < r),
r' : ℝ≥0,
_inst_6 : fact (0 < r'),
_inst_7 : fact (r' ≤ 1),
M : ProFiltPseuNormGrpWithTinv r',
c N : ℝ≥0
⊢ ∀ (i j : ℕ), universal_map.suitable (r' * (c * (c' j * N⁻¹))) (r' * (c * (c' i * N⁻¹))) (BD.d j i)

BD : data,
c' : ℕ → ℝ≥0,
_inst_1 : BD.suitable c',
r : ℝ≥0,
V : NormedGroup,
_inst_4 : normed_with_aut ↑r V,
_inst_5 : fact (0 < r),
r' : ℝ≥0,
_inst_6 : fact (0 < r'),
_inst_7 : fact (r' ≤ 1),
M : ProFiltPseuNormGrpWithTinv r',
c N : ℝ≥0
⊢ ∀ (i j : ℕ), universal_map.suitable (c * (c' j * N⁻¹)) (c * (c' i * N⁻¹)) (BD.d j i)

BD : data,
c' : ℕ → ℝ≥0,
_inst_1 : BD.suitable c',
r : ℝ≥0,
V : NormedGroup,
_inst_4 : normed_with_aut ↑r V,
_inst_5 : fact (0 < r),
r' : ℝ≥0,
_inst_6 : fact (0 < r'),
_inst_7 : fact (r' ≤ 1),
M : ProFiltPseuNormGrpWithTinv r',
c N : ℝ≥0
⊢ ?m_1 =
cochain_complex.mk
(λ (i : ℕ),
(BD.complex₂_X r V r' (λ (i : ℕ), c * c' i) (λ (i : ℕ), r' * (c * c' i)) i).obj
(opposite.op (of r' (rescale N ↥M))))
(λ (i j : ℕ),
(universal_map.eval_CLCFPTinv₂ r V r' (c * c' i) (r' * (c * c' i)) (c * c' j) (r' * (c * c' j))
(BD.d j i)).app
(opposite.op (of r' (rescale N ↥M))))
_
_


#### Sebastian Ullrich (Mar 30 2021 at 21:34):

For the vim weirdos like me, perhaps the best solution would be to put explicit support into the extension to shift the goal request position appropriately when in normal mode. Doesn't work for the Lean 3 "at end of tactic" approach though.

#### Mario Carneiro (Mar 30 2021 at 21:35):

First, I have to scroll past the tactic state, which has four goals that have nothing wrong with them, to see the error message: "simplify tactic failed to simplify". Then I have to scroll some more past the long context to find the actual goal ⊢ bar BD r V M (λ (i : ℕ), r' * (c * (c' i * N⁻¹))) (λ (i : ℕ), c * (c' i * N⁻¹)) ?m_1 ?m_2 _ _ = ?m_3 that failed to simplify

#### Mario Carneiro (Mar 30 2021 at 21:35):

The information that is most relevant is buried under a mountain of noise

#### Mario Carneiro (Mar 30 2021 at 21:36):

This isn't even a particularly large context. It gets a lot worse than this

#### Daniel Fabian (Mar 30 2021 at 21:38):

@Mario Carneiro one thing that's an interesting observation is, that most of the state is actually duplicate. I wonder how much better it would look if we did a tree-like structure where the common things are shared and only the differences shown in each state?

#### Julian Berman (Mar 30 2021 at 21:38):

Is part of that to do with the goal state being included in the diagnostic message? Maybe the server should just respond with the error itself and the spot it occurs in the diagnostic, and if you want the tactic state too you do a hover separately?

#### Mario Carneiro (Mar 30 2021 at 21:39):

Putting the |- part first would also help with the long context problem, although it is a bit weird

#### Mario Carneiro (Mar 30 2021 at 21:42):

One way to address the duplicate context problem is to elide the context from all goals other than the first. That's not quite the same as doing a tree like thing but I don't know how to present that in a way such that you can reconstruct everything

#### Mario Carneiro (Mar 30 2021 at 21:44):

3 goals
⊢ a = b
A : Type
a : A
b : A

... ⊢ c = d
... ⊢ a = a


#### Daniel Fabian (Mar 30 2021 at 21:46):

Tactic state:
4 goals
BD : data,
c' : ℕ → ℝ≥0,
_inst_1 : BD.suitable c',
r : ℝ≥0,
V : NormedGroup,
_inst_4 : normed_with_aut ↑r V,
_inst_5 : fact (0 < r),
r' : ℝ≥0,
_inst_6 : fact (0 < r'),
_inst_7 : fact (r' ≤ 1),
M : ProFiltPseuNormGrpWithTinv r',
c N : ℝ≥0
---------------
⊢ bar BD r V M (λ (i : ℕ), r' * (c * (c' i * N⁻¹))) (λ (i : ℕ), c * (c' i * N⁻¹)) ?m_1 ?m_2 _ _ = ?m_3

⊢ ∀ (i j : ℕ), universal_map.suitable (r' * (c * (c' j * N⁻¹))) (r' * (c * (c' i * N⁻¹))) (BD.d j i)

⊢ ∀ (i j : ℕ), universal_map.suitable (c * (c' j * N⁻¹)) (c * (c' i * N⁻¹)) (BD.d j i)


#### Daniel Fabian (Mar 30 2021 at 21:46):

you'd have the bar to separate shared from non-shared

#### Daniel Fabian (Mar 30 2021 at 21:46):

thus for the 2 other goals you might have additional context

#### Mario Carneiro (Mar 30 2021 at 21:47):

What if the main goal has more context than the other two?

#### Daniel Fabian (Mar 30 2021 at 21:48):

then you put the line higher.

#### Daniel Fabian (Mar 30 2021 at 21:48):

it's just a common-prefix thing

Oh I see

#### Mario Carneiro (Mar 30 2021 at 21:49):

Also, can we remove the commas from the proof goal display? It's annoying to edit those out when copying it into a def or something

#### Mario Carneiro (Mar 30 2021 at 21:49):

especially since the last hypothesis doesn't have a comma

#### Mario Carneiro (Mar 30 2021 at 21:52):

What if you put the common context last:

Tactic state:
4 goals
⊢ bar BD r V M (λ (i : ℕ), r' * (c * (c' i * N⁻¹))) (λ (i : ℕ), c * (c' i * N⁻¹)) ?m_1 ?m_2 _ _ = ?m_3

i j : ℕ
⊢ universal_map.suitable (r' * (c * (c' j * N⁻¹))) (r' * (c * (c' i * N⁻¹))) (BD.d j i)

⊢ ∀ (i j : ℕ), universal_map.suitable (c * (c' j * N⁻¹)) (c * (c' i * N⁻¹)) (BD.d j i)

context:
BD : data,
c' : ℕ → ℝ≥0,
_inst_1 : BD.suitable c',
r : ℝ≥0,
V : NormedGroup,
_inst_4 : normed_with_aut ↑r V,
_inst_5 : fact (0 < r),
r' : ℝ≥0,
_inst_6 : fact (0 < r'),
_inst_7 : fact (r' ≤ 1),
M : ProFiltPseuNormGrpWithTinv r',
c N : ℝ≥0


Maybe the context is even in a separate dropdown

#### Daniel Fabian (Mar 30 2021 at 21:52):

come to think of it, if we did the compression by common prefix or something, then even showing the proof state both before and after might be feasible

#### Daniel Fabian (Mar 30 2021 at 21:53):

that blows up in your face if you have 20 goals

#### Daniel Fabian (Mar 30 2021 at 21:53):

but you could do it for just the first goal for instance

#### Mario Carneiro (Mar 30 2021 at 21:53):

that's true, it would be best to have the context after the first goal

#### Mario Carneiro (Mar 30 2021 at 21:54):

or even before the first goal, provided the first goal is always on screen first and there is a way to draw the reader's attention to it

#### Mario Carneiro (Mar 30 2021 at 21:54):

I do like the visual effect of the variable moving up into the context when you do an intro

#### Daniel Fabian (Mar 30 2021 at 21:55):

like for instance clamped to the bottom of the window?

right

#### Daniel Fabian (Mar 30 2021 at 21:55):

in fact, I do like the shared context for another reason, too.

#### Mario Carneiro (Mar 30 2021 at 21:55):

but you also want to show the error message and the other goals and they can't all fit

#### Daniel Fabian (Mar 30 2021 at 21:55):

say you have 5 similar goals.

#### Daniel Fabian (Mar 30 2021 at 21:56):

then doing an all_goals {x y z} becomes much easier if you see the goals instead of mostly context.

#### Jasmin Blanchette (Apr 02 2021 at 05:43):

I'm in favor of |intro or, perhaps best, i|ntro. The old behavior, while "theoretically" justifiable, almost always showed the wrong subgoal until you learned to artificially move the cursor past the comma.

#### Damiano Testa (Apr 02 2021 at 06:01):

I am also in favour of i|ntro: for me this is the best option!

#### Daniel Fabian (Apr 02 2021 at 16:18):

does anyone have feedback on the idea of collapsing shared context?

#### Greg Price (Apr 02 2021 at 16:27):

I think the common-prefix idea sounds great.

#### Julian Berman (Apr 02 2021 at 16:57):

Not sure if this is helpful or already considered but hopefully there's a difference between the message as presented in vscode and the actual response from the server? Like it'd be nice if one could separate the actual pieces of the context (because they're structurally separate in the server response), regardless of how they're ultimately showed to a human

#### Daniel Fabian (Apr 02 2021 at 17:35):

right now, the context in lean4 is passed almost verbatim from the server. This approach has both good and bad sides. One nice thing is, that you can write most of the logic in lean, the not-so-nice part is, that the extension is somewhat limited in what it can do.

In lean3 the object model with widgets is more complex, but I don't know the details there.

#### Julian Berman (Apr 02 2021 at 17:42):

I guess I don't know enough about widgets either, I thought they were more about how you create graphical interaction on the client-side, whereas I guess I'm asking more about ways the server communicates structured data -- similar I guess to how if you have the simp? tactic and it wants to say "here are my simp lemmas", in lean3 that's a bunch of hairy text, not structured data -- it's just "Try this: bla" and you get to parse that (simple) text. Rather than some protocol the server (or tactic definition) speaks, where you can say (e.g. in JSON): {"response": {"simp-lemmas": ["foo", "bar"]}} and then how you render that (e.g. as Try this: foo\n Try this: bar\n) is up to the client (vscode extension or whatever)

#### Julian Berman (Apr 02 2021 at 17:43):

(And here like {"response": {"error": "whatever", "summary": thatCompressedTreeMessage, "state": justTheTacticState}})

#### Sebastian Ullrich (Apr 02 2021 at 17:47):

For "Try this" etc, the LSP spec already gives us the expected format (it should be a "code action"). The goal view is special in that it is a custom extension of the protocol.

#### Julian Berman (Apr 02 2021 at 17:48):

Makes sense -- and that custom extension just speaks plaintext essentially?

#### Julian Berman (Apr 02 2021 at 17:49):

a ha, ok, so there's a couple more things, but this is about that rendered field

#### Sebastian Ullrich (Apr 02 2021 at 17:50):

which afaik is not used by either extension anymore

#### Daniel Fabian (Apr 02 2021 at 18:01):

Well, if we did go down the route of implementing the prefix compression, we should have a structure more or less like this:

structure PlainGoal where
rendered : String
prefix : String
goals : Array String


So that you can easily get the old behaviour but just prefix.map (fun x => prefix ++ x), but you could also get the compressed prefix rendering if so desired.

#### Daniel Fabian (Apr 02 2021 at 18:04):

on the other hand, we still want lean's pretty printer to take care of the heavy lifting. That's not something you want to implement in the extension.

#### Sebastian Ullrich (Apr 02 2021 at 22:39):

Jasmin Blanchette said:

I'm in favor of |intro or, perhaps best, i|ntro. The old behavior, while "theoretically" justifiable, almost always showed the wrong subgoal until you learned to artificially move the cursor past the comma.

Good to hear that someone else actually finds the Lean 3 behavior problematic :)

#### Sebastian Ullrich (Apr 02 2021 at 22:41):

I've now implemented Mario's i|ntro proposal, please give it a try. We also now show goals from all execution branches (e.g. after <;>) at the current position, feedback on that would be valuable as well.

#### Julian Berman (Apr 02 2021 at 23:57):

Well it works :) and I indeed got it working in vim normal mode hee hee https://asciinema.org/a/GARVUQZtmHeGeKxOBqVO18dAC (don't look at my newbie lean code but it does work hooray)

#### Julian Berman (Apr 03 2021 at 00:14):

I think after a few minutes though that in my case it's a bit awkward that it's on the second character, but I guess I'll try shifting the request by 1 on my side.

#### Sebastian Ullrich (May 02 2021 at 17:45):

I've now refined the i|ntro logic in https://github.com/leanprover/lean4/pull/434: if the tactic looks like a combinator (has a nested tactic not surrounded by by), we default to showing the initial goal on the outer tactic. Thus if you put your cursor at i|nduction ... with ..., it will no longer show you a useless "goals accomplished". Combinators can and should override this default behavior where sensible, and we do so for induction/cases/case/match, showing the corresponding case goal on the ... => part. Oh, and we show the initial goal on by, even if you haven't written anything after it yet.

#### Lucas V. (May 04 2021 at 17:30):

Julian Berman said:

Well it works :) and I indeed got it working in vim normal mode hee hee https://asciinema.org/a/GARVUQZtmHeGeKxOBqVO18dAC (don't look at my newbie lean code but it does work hooray)

Hi, sorry if this is the wrong place to ask, but is there a way to have this infoview in emacs?

#### Sebastian Ullrich (May 04 2021 at 17:35):

Yes, press C-c C-i :)

#### Sebastian Ullrich (May 04 2021 at 17:35):

(lean4-toggle-info in recent lean4-mode)

#### Lucas V. (May 04 2021 at 17:46):

Thanks! So this almost works, it tries to display the goal but this error pops up in the message buffer instead:

Error processing message (wrong-type-argument listp #s(hash-table size 1 test equal rehash-size 1.5 rehash-threshold 0.8125 data ("rendered" "lean
m n k : Nat
⊢ succ (n + (m + k)) = succ (n + (m + k))
"))).


I tried with lean4 stable and nighly. Maybe this is a problem with my lsp-mode? I'm using its latest version too.

#### Lucas V. (May 04 2021 at 17:47):

And I am also using the latest lean4-mode from the lean4 repo

Last updated: May 18 2021 at 23:14 UTC