goal view

Stream: lean4

[Reid Barton]

There's no goal view yet right?

[Kenny Lau]

there is the problems panel on the bottom

[Adam Topaz]

In emacs the "next error" window works.

[Reid Barton]

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

[Reid Barton]

I guess "make an error happen" works

[Reid Barton]

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

[Julian Berman]

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]

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:
The adapted Lean 3 approach:

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]

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]

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]

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

[Sebastian Ullrich]

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

[Sebastian Ullrich]

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]

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

[Mario Carneiro]

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]

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]

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]

@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]

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]

(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]

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

[Mario Carneiro]

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]

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]

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]

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]

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]

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]

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

[Mario Carneiro]

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

[Daniel Fabian]

@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]

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]

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

[Mario Carneiro]

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]

How about this:

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

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

[Daniel Fabian]

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]

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

[Daniel Fabian]

thus for the 2 other goals you might have additional context

[Mario Carneiro]

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

[Daniel Fabian]

then you put the line higher.

[Daniel Fabian]

it's just a common-prefix thing

[Mario Carneiro]

Oh I see

[Mario Carneiro]

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]

especially since the last hypothesis doesn't have a comma

[Mario Carneiro]

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]

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]

that blows up in your face if you have 20 goals

[Daniel Fabian]

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

[Mario Carneiro]

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

[Mario Carneiro]

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]

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

[Daniel Fabian]

like for instance clamped to the bottom of the window?

[Mario Carneiro]

right

[Daniel Fabian]

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

[Mario Carneiro]

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

[Daniel Fabian]

say you have 5 similar goals.

[Daniel Fabian]

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

[Jasmin Blanchette]

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]

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

[Daniel Fabian]

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

[Greg Price]

I think the common-prefix idea sounds great.

[Julian Berman]

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]

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]

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]

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

[Sebastian Ullrich]

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]

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

[Sebastian Ullrich]

Not quite https://github.com/leanprover/lean4/blob/master/src/Lean/Data/Lsp/Extra.lean#L40-L42

[Julian Berman]

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

[Sebastian Ullrich]

which afaik is not used by either extension anymore

[Daniel Fabian]

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]

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]

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]

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]

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]

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]

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

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]

Yes, press C-c C-i :)

[Sebastian Ullrich]

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

[Lucas V.]

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

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

[Lucas Viana]

Today I figured out the problem:

Maybe due to other package I am using or maybe because it's emacs 28, when the goal view is created the cursor moves to the goal view. So when lean4-toggle-info calls (lean4-info-buffer-refresh) it is not at the Lean4 buffer and some lsp functions throw the error.

Simply removing the (lean4-info-buffer-refresh) line solves the problem, but the right fix would probably be a bit more sophisticated