VScode message window

Stream: general

[Johan Commelin]

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]

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

[Johan Commelin]

That's already really nice

[Alexander Bentkamp]

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

[Alexander Bentkamp]

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]

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]

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]

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]

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

[Gabriel Ebner]

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:"?

[Johan Commelin]

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

[Johan Commelin]

If that isn't too tricky...

[Rob Lewis]

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

[Alexander Bentkamp]

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]

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

[Rob Lewis]

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

[Mario Carneiro]

Can the lean parser report this information?

[Rob Lewis]

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]

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

[Mario Carneiro]

next unbracketed (comma or semicolon or newline) I think

[Rob Lewis]

Yeah, e.g.

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

reports the message only at squeeze_simp.

[Mario Carneiro]

I can imagine stuff like

simp [foo, bar,
  baz]

so bracket matching is important, I think

[Mario Carneiro]

There are still some outliers I can think of, like

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

[Johan Commelin]

But rcases is not a problem right?

[Johan Commelin]

Because then you just need to replace rcases?

[Bryan Gin-ge Chen]

Another example is:

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

[Mario Carneiro]

that's bracketed so it's okay

[Rob Lewis]

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]

(by bracketed I mean tracking all bracket characters)

[Johan Commelin]

The proper solution would be to reimplement VScode in Lean.

[Mario Carneiro]

or lean in vscode...

[Mario Carneiro]

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]

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

[Mario Carneiro]

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

[Patrick Massot]

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

[Patrick Massot]

But it's still all very nice!

[Alexander Bentkamp]

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