## Stream: general

### Topic: VScode message window

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

#### 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 :-)

#### 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)

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

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

#### 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).

#### 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?

#### 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


#### 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_smul f,
linear_map.map_smul₂ f,
sub_self,
free_abelian_group.lift.of,
free_abelian_group.lift.neg,


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

#### Johan Commelin (Feb 19 2020 at 14:50):

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

#### Johan Commelin (Feb 19 2020 at 14:50):

If that isn't too tricky...

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

#### 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?

#### Rob Lewis (Feb 19 2020 at 20:09):

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

#### Rob Lewis (Feb 19 2020 at 20:11):

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

#### Mario Carneiro (Feb 19 2020 at 20:11):

Can the lean parser report this information?

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

#### Mario Carneiro (Feb 19 2020 at 20:16):

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

#### Mario Carneiro (Feb 19 2020 at 20:17):

next unbracketed (comma or semicolon or newline) I think

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

#### Mario Carneiro (Feb 19 2020 at 20:19):

I can imagine stuff like

simp [foo, bar,
baz]


so bracket matching is important, I think

#### 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⟩,


#### Johan Commelin (Feb 19 2020 at 20:22):

But rcases is not a problem right?

#### Johan Commelin (Feb 19 2020 at 20:23):

Because then you just need to replace rcases?

#### Bryan Gin-ge Chen (Feb 19 2020 at 20:23):

Another example is:

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


#### Mario Carneiro (Feb 19 2020 at 20:23):

that's bracketed so it's okay

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

#### Mario Carneiro (Feb 19 2020 at 20:24):

(by bracketed I mean tracking all bracket characters)

#### Johan Commelin (Feb 19 2020 at 20:25):

The proper solution would be to reimplement VScode in Lean.

#### Mario Carneiro (Feb 19 2020 at 20:25):

or lean in vscode...

#### 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 ⦄⟩}])

#### Patrick Massot (Feb 19 2020 at 20:27):

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

#### Mario Carneiro (Feb 19 2020 at 20:27):

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

#### Patrick Massot (Feb 19 2020 at 20:30):

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

#### Patrick Massot (Feb 19 2020 at 20:30):

But it's still all very nice!

#### 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