Zulip Chat Archive

Stream: lean4

Topic: goal view


view this post on Zulip Reid Barton (Jan 11 2021 at 15:12):

There's no goal view yet right?

view this post on Zulip Kenny Lau (Jan 11 2021 at 15:21):

there is the problems panel on the bottom

view this post on Zulip Adam Topaz (Jan 11 2021 at 15:22):

In emacs the "next error" window works.

view this post on Zulip 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?

view this post on Zulip Reid Barton (Jan 11 2021 at 15:27):

I guess "make an error happen" works

view this post on Zulip Reid Barton (Jan 11 2021 at 19:02):

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

view this post on Zulip 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

view this post on Zulip 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:
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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip 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].

view this post on Zulip 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.

view this post on Zulip Mario Carneiro (Mar 30 2021 at 21:21):

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

view this post on Zulip 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

view this post on Zulip 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)

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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 <=

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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))))
      _
      _

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Mar 30 2021 at 21:35):

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

view this post on Zulip Mario Carneiro (Mar 30 2021 at 21:36):

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

view this post on Zulip 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?

view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Mar 30 2021 at 21:44):

How about this:

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

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

view this post on Zulip 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)

view this post on Zulip Daniel Fabian (Mar 30 2021 at 21:46):

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

view this post on Zulip Daniel Fabian (Mar 30 2021 at 21:46):

thus for the 2 other goals you might have additional context

view this post on Zulip Mario Carneiro (Mar 30 2021 at 21:47):

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

view this post on Zulip Daniel Fabian (Mar 30 2021 at 21:48):

then you put the line higher.

view this post on Zulip Daniel Fabian (Mar 30 2021 at 21:48):

it's just a common-prefix thing

view this post on Zulip Mario Carneiro (Mar 30 2021 at 21:49):

Oh I see

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Mar 30 2021 at 21:49):

especially since the last hypothesis doesn't have a comma

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Daniel Fabian (Mar 30 2021 at 21:53):

that blows up in your face if you have 20 goals

view this post on Zulip Daniel Fabian (Mar 30 2021 at 21:53):

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

view this post on Zulip Mario Carneiro (Mar 30 2021 at 21:53):

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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Daniel Fabian (Mar 30 2021 at 21:55):

like for instance clamped to the bottom of the window?

view this post on Zulip Mario Carneiro (Mar 30 2021 at 21:55):

right

view this post on Zulip Daniel Fabian (Mar 30 2021 at 21:55):

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

view this post on Zulip 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

view this post on Zulip Daniel Fabian (Mar 30 2021 at 21:55):

say you have 5 similar goals.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Damiano Testa (Apr 02 2021 at 06:01):

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

view this post on Zulip Daniel Fabian (Apr 02 2021 at 16:18):

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

view this post on Zulip Greg Price (Apr 02 2021 at 16:27):

I think the common-prefix idea sounds great.

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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)

view this post on Zulip Julian Berman (Apr 02 2021 at 17:43):

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

view this post on Zulip 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.

view this post on Zulip Julian Berman (Apr 02 2021 at 17:48):

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

view this post on Zulip Sebastian Ullrich (Apr 02 2021 at 17:49):

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

view this post on Zulip 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

view this post on Zulip Sebastian Ullrich (Apr 02 2021 at 17:50):

which afaik is not used by either extension anymore

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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 :)

view this post on Zulip 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.

view this post on Zulip 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)

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip Sebastian Ullrich (May 04 2021 at 17:35):

Yes, press C-c C-i :)

view this post on Zulip Sebastian Ullrich (May 04 2021 at 17:35):

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

view this post on Zulip 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.

view this post on Zulip 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