Zulip Chat Archive

Stream: general

Topic: VScode message window


view this post on Zulip Johan Commelin (Feb 13 2020 at 06:39):

We now have several tactics that report back with tactic scripts in the Lean messages window: squeeze_simp, tidy?, suggest, extract_goal and in a couple of days hint. Would it be possible to hit C-x M-c M-butterfly and magically have the tactic-script-reporting-tactic under the cursor be replaces with whatever tactic script it reported?
I understand that maybe this would require that the tactic script reports follow a common output format, but that shouldn't be hard.

In principle hole commands would do this. But in practice, that doesn't seem to work. (They work great for dumping a skeleton of a structure, and things like that.) For one, the hole command wouldn't let you inspect the reported script, before hitting the magic keyboard combo.

view this post on Zulip Alexander Bentkamp (Feb 14 2020 at 09:14):

I thought this would be a good opportunity for me to experiment with the VSCode extension. I already have something now that kind of works:

https://github.com/leanprover/vscode-lean/pull/143

For now, it copies the entire message of the tactic (which is what we want for the current implementation of squeeze_simp) and replaces the current selection (i.e., you need to select the characters squeeze_simp in your editor before you press the key combination for this to work properly). So there is a lot of room for improvement :-)

view this post on Zulip Johan Commelin (Feb 14 2020 at 09:17):

That's already really nice

view this post on Zulip Alexander Bentkamp (Feb 14 2020 at 09:18):

What would be the best key combination for this? I currently have alt+v. (v like pasting in ctrl+v)

view this post on Zulip Alexander Bentkamp (Feb 14 2020 at 09:21):

And what should be the format for the tactic output? We could change squeeze_simp to say:

Try this: simp only [foo, bar]

This is what Isabelle/Sledgehammer says, too. Then the words "Try this:" could be recognized by the extension.

view this post on Zulip Gabriel Ebner (Feb 14 2020 at 14:24):

This is a great idea!

  • There should really be a magic string like Try this: that is recognized by the extension. You should also be able to print additional stuff from the tactic before/after the Try this:.
  • You shouldn't have to select the tactic invocation before calling alt+v. There is no way to obtain the range of the tactic (i.e. where squeeze_simp or library_search is in the file). But as a first heuristic, just selecting everything from the position of the message until the end of the line (or the next comma) should work in most cases.

view this post on Zulip Gabriel Ebner (Feb 14 2020 at 14:25):

If this works nicely, I'd also like to integrate it in the info view, so that you can click on the Try this: (or some button right next to it).

view this post on Zulip Rob Lewis (Feb 19 2020 at 09:43):

A very minor bug report/feature request: when you use this on a tactic call with a trailing comma, it deletes the comma. Would it be possible to replace until the next unbracketed comma instead of the end of the line? Or is there an ambiguity there I'm not seeing?

view this post on Zulip Rob Lewis (Feb 19 2020 at 09:43):

example (a : ) (h : a = 0) : a = 1 - 1 :=
begin
  squeeze_simp, -- inserting the suggestion breaks the proof
  exact h
end

view this post on Zulip Gabriel Ebner (Feb 19 2020 at 11:15):

Another bug report: when squeeze_simp suggests a long tactic that spans over multiple lines, only the first line is pasted:

Try this: simp only [is_add_group_hom.mem_ker,
 linear_map.map_add f,
 linear_map.map_add₂ f,
 linear_map.map_smul f,
 linear_map.map_smul₂ f,
 sub_self,
 free_abelian_group.lift.of,
 add_comm,
 add_right_neg,
 add_add_neg_cancel'_right,
 neg_add_rev,
 free_abelian_group.lift.add,
 free_abelian_group.lift.neg,
 sub_eq_add_neg,
 add_left_comm]

Should squeeze_simp etc. just everything on a single line, or should the vscode extension also include indented lines after the "Try this:"?

view this post on Zulip Johan Commelin (Feb 19 2020 at 14:50):

Hmm, maybe including all indented lines is a good compromise.

view this post on Zulip Johan Commelin (Feb 19 2020 at 14:50):

If that isn't too tricky...

view this post on Zulip Rob Lewis (Feb 19 2020 at 14:55):

Yes, I'd prefer all indented lines instead of having the tactics print a single long line.

view this post on Zulip Alexander Bentkamp (Feb 19 2020 at 20:07):

Rob Lewis said:

A very minor bug report/feature request: when you use this on a tactic call with a trailing comma, it deletes the comma. Would it be possible to replace until the next unbracketed comma instead of the end of the line? Or is there an ambiguity there I'm not seeing?

How far should be replaced if the code says something like by squeeze_simp? Then there is no comma. Maybe the code should check whether the tactic is preceded by by to recognize this situation?

view this post on Zulip Rob Lewis (Feb 19 2020 at 20:09):

The next comma, EOL, or unmatched close paren, whichever comes first?

view this post on Zulip Rob Lewis (Feb 19 2020 at 20:11):

Maybe the grammar here is too complicated to be worth implementing, heh.

view this post on Zulip Mario Carneiro (Feb 19 2020 at 20:11):

Can the lean parser report this information?

view this post on Zulip Rob Lewis (Feb 19 2020 at 20:14):

Honestly, "until the next line break" is like 95% of what you need and it's nice to keep the implementation entirely in the VSCode extension.

view this post on Zulip Mario Carneiro (Feb 19 2020 at 20:16):

Oh I see, vscode only gets the first word of the tactic?

view this post on Zulip Mario Carneiro (Feb 19 2020 at 20:17):

next unbracketed (comma or semicolon or newline) I think

view this post on Zulip Rob Lewis (Feb 19 2020 at 20:18):

Yeah, e.g.

example : true  true :=
by squeeze_simp [nat.succ_pos]

reports the message only at squeeze_simp.

view this post on Zulip Mario Carneiro (Feb 19 2020 at 20:19):

I can imagine stuff like

simp [foo, bar,
  baz]

so bracket matching is important, I think

view this post on Zulip Mario Carneiro (Feb 19 2020 at 20:20):

There are still some outliers I can think of, like

rcases (very long expr)
  with very, long, pattern,

view this post on Zulip Johan Commelin (Feb 19 2020 at 20:22):

But rcases is not a problem right?

view this post on Zulip Johan Commelin (Feb 19 2020 at 20:23):

Because then you just need to replace rcases?

view this post on Zulip Bryan Gin-ge Chen (Feb 19 2020 at 20:23):

Another example is:

tidy? {
  tactics := [tactic1,
    tactic2]
}

view this post on Zulip Mario Carneiro (Feb 19 2020 at 20:23):

that's bracketed so it's okay

view this post on Zulip Rob Lewis (Feb 19 2020 at 20:23):

I think we can grant that it won't be perfect and "next unbracketed (comma or semicolon or newline)" is a good (and easy?) approximation.

view this post on Zulip Mario Carneiro (Feb 19 2020 at 20:24):

(by bracketed I mean tracking all bracket characters)

view this post on Zulip Johan Commelin (Feb 19 2020 at 20:25):

The proper solution would be to reimplement VScode in Lean.

view this post on Zulip Mario Carneiro (Feb 19 2020 at 20:25):

or lean in vscode...

view this post on Zulip Mario Carneiro (Feb 19 2020 at 20:26):

Since lean is handling all the high level bracket matching, I think you can just keep a single counter, increase it every time you see ([{⟨⦃ and decrease on ⦄⟩}])

view this post on Zulip Patrick Massot (Feb 19 2020 at 20:27):

I just tried that "Try this" thing, and it eats my commas.

view this post on Zulip Mario Carneiro (Feb 19 2020 at 20:27):

Maybe if you click on the colon in "Try this:" it will put the punctuation in

view this post on Zulip Patrick Massot (Feb 19 2020 at 20:30):

Also the tooltip when hovering over a suggestion is pretty distracting (and uninformative).

view this post on Zulip Patrick Massot (Feb 19 2020 at 20:30):

But it's still all very nice!

view this post on Zulip Alexander Bentkamp (Feb 20 2020 at 22:44):

Thanks for the feedback! https://github.com/leanprover/vscode-lean/pull/144


Last updated: May 06 2021 at 22:13 UTC