## Stream: general

### Topic: vscode extension

#### Gabriel Ebner (May 14 2020 at 13:51):

The vscode extension now has two new features:

• ctrl+shift+p sticky: allows you to sticky the infoview at the current position. It will keep updating and show the errors at the original position even if you edit somewhere else. Thanks to @Mario Carneiro
• The see note [sandwich] comments are linkified.

#### Johan Commelin (May 14 2020 at 14:25):

But how about ctrl + shift + p -- "Lean restart"?

#### Daniel Fabian (May 14 2020 at 19:13):

Is there a feature like paste the current goal?

A long chain of tactics is very convenient to write, but basically impossible to read without vscode. So sometimes it'd be very, add a show [paste current goal here] or a calc [paste current goal here] just to make the proof easier to read.

However as it stands now, the moment you write show or calc it wipes the proof state and you basically don't know what you're trying to write.

#### Johan Commelin (May 14 2020 at 19:13):

There is a tactic extract_goal

#### Johan Commelin (May 14 2020 at 19:13):

It's not exactly what you describe

#### Johan Commelin (May 14 2020 at 19:14):

I usually write

/-
-/


and then paste the goal in it.

#### Daniel Fabian (May 14 2020 at 19:14):

we have an alt+v for things like library_search, right?

#### Johan Commelin (May 14 2020 at 19:14):

After that, I prepend show, or calc, or change, etc...

#### Daniel Fabian (May 14 2020 at 19:15):

ya, same, lol. Alternatively you can pause the goal. Which would be ok, if you could keybind it, I suppose.

#### Johan Commelin (May 14 2020 at 19:15):

You can keybind it

#### Johan Commelin (May 14 2020 at 19:15):

I saw discussion a couple of days ago. Haven't done it myself

#### Daniel Fabian (May 14 2020 at 19:15):

oh, what's the command called?

#### Johan Commelin (May 14 2020 at 19:15):

Something with freeze or sticky, I guess

#### Alex J. Best (May 14 2020 at 19:16):

https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/topic/lean.20for.20coq.20users.3F/near/196924597

#### Johan Commelin (May 14 2020 at 19:16):

Do you have the newest VScode lean extension? One was released today, I think.

#### Bryan Gin-ge Chen (May 14 2020 at 19:16):

Search for "toggle updating" in the keyboard shortcuts.

#### Bryan Gin-ge Chen (May 14 2020 at 19:17):

There's also a very new feature that freezes the position that's being inspected in the goal window. I haven't played around with that yet.

#### Daniel Fabian (May 14 2020 at 19:17):

there's sticky position

#### Daniel Fabian (May 14 2020 at 19:21):

oh, it doesn't show up in the commands but DOES show up in the keybindings. Ok that's just simply confusing :P

#### Bryan Gin-ge Chen (May 14 2020 at 19:25):

We could easily add it to the commands. I'll open a PR to do it later tonight if no one beats me to it.

#### Daniel Fabian (May 14 2020 at 19:27):

As a general rule, I think we should have the commands available through the commands panel. Until today I didn't even know that it was possible for a keybind to not show up in the commands list.

#### Bryan Gin-ge Chen (May 15 2020 at 01:59):

This ended up being a bigger PR than I thought it would be: leanprover/vscode-lean#161 .

#### Bryan Gin-ge Chen (Jun 19 2020 at 16:06):

Does anyone have any useful "tactic state filters" they use frequently (beyond the two included by default)? @Edward Ayers is looking for a few test cases.

#### Edward Ayers (Jun 19 2020 at 16:07):

I've found some in the default config of vscode

#### Edward Ayers (Jun 19 2020 at 16:07):

So far I've got:

[
{
"regex": "^_",
"match": false,
"flags": ""
},
{
"name": "goals only",
"regex": "^(⊢|\\d+ goals|case|\$)",
"match": true,
"flags": ""
}
],


#### Kevin Buzzard (Jun 19 2020 at 16:39):

I'd be keen to see a filter which doesn't make it say no info found at scratch6.lean:1:2 at the top at all times.

#### Edward Ayers (Jun 19 2020 at 16:41):

Would it be better to just not show anything?

#### Kevin Buzzard (Jun 19 2020 at 16:43):

My instinct as a user (I've been using the widget stuff for about 24 hours now) is that whenever I'm in the middle of a proof, I just want to look at the very top of the output on the right and see my current goal. I found it a bit disorientating that there was always something above it.

#### Edward Ayers (Jun 19 2020 at 16:44):

:/ It shouldn't show no info found if the current goal is there

#### Edward Ayers (Jun 19 2020 at 16:50):

lean-0.15.15.vsix

#### Kevin Buzzard (Jun 19 2020 at 22:29):

Oh, my current version shows "Error updating: . Try again." at the top of lean goal mode. I'll try updating.

#### Kevin Buzzard (Jun 19 2020 at 22:30):

ooh that fixed it

#### Yakov Pechersky (Jun 24 2020 at 06:42):

In VSCode over Remote-SSH, in the public lean extension (0.15.x), the freeze/unfreeze button is wonky:

image.png

#### Gabriel Ebner (Jun 24 2020 at 07:46):

Yes, loading local resources is pretty broken in vscode at the moment. https://github.com/microsoft/vscode/issues/89038 There was a fix planned for this month's release, but the fix is delayed.
As a workaround, we're running an http server on localhost. I'm not surprised this doesn't work over ssh.

#### Daniel Fabian (Jul 18 2020 at 15:20):

Any idea how hard/easy it would be to provide some rudimentary refactoring? We have go to definition and peek definition. One that I feel is missing and would be super helpful would be rename. This is not just a simple regex replace, because of variable shadowing, so we'd want the right variable to be renamed.

#### Bryan Gin-ge Chen (Jul 18 2020 at 17:01):

I agree this would be really helpful, but it seems like it would be pretty difficult to me. VS Code does provide an API for extensions to perform "symbol renames", however we would need a new Lean server command that would be able to search through all files in the project and figure out what edits would be appropriate.

As far as I know, the Lean 3 server doesn't currently have any way to search through files without opening them, so for a gigantic project like mathlib, that might take a very long time. I'm also not sure whether Lean currently remembers anything about the syntactic form of defs / theorems / proofs (other than where declarations are initially defined).

I seem to recall @Johan Commelin had some secret tool using lean-client-python that could do some of this though?

#### Johan Commelin (Jul 18 2020 at 17:04):

It was actually @Jason Rute that wrote the secret tool

#### Daniel Fabian (Jul 18 2020 at 19:15):

Oh I see. When I asked about this, I wasn't so much thinking large-scale refactoring as more like rename an m to an s inside of a function.

#### Daniel Fabian (Jul 18 2020 at 19:16):

would that be easier?

#### Bryan Gin-ge Chen (Jul 18 2020 at 21:04):

Not sure. Like I said, the Lean server doesn't have functionality like this currently so it would have to be added in any case. Feel free to create an issue at https://github.com/leanprover-communtiy/lean/issues but it might be something that won't appear before Lean 4.

#### Bryan Gin-ge Chen (Jul 18 2020 at 21:05):

It also depends on how good the secret tool is; hopefully @Jason Rute will show up and say more...

#### Jason Rute (Jul 18 2020 at 22:10):

The "secret tool" is not so much as a secret as something that isn't as developed as it could be. The code is here (currently in its own branch): https://github.com/leanprover-community/lean-client-python/blob/find-and-replace-example/examples/find_and_replace.py

#### Jason Rute (Jul 18 2020 at 22:10):

Basically it is a fairly simple use case of the lean server, specifically Patrick's lean-client for python. We first find all strings of the desired form and then use the lean server to check if they are instances of the definition in question. It will only work for instances that the lean server info command works on. So it won't say work on the original definition (but that particular case could be fixed.) Depending on the number of instances of the string it could take from minutes to hours to refactor.

#### Jason Rute (Jul 18 2020 at 22:10):

The reason that this tool is not as developed as it could be is:

1. The Lean client for python is still going through some significant bug fixes. I dropped the ball here, but will try to finish them up.
2. This is really just a quick implementation of an idea. (I wrote it in an afternoon.) If someone is more ambitious (and knows about Python's await), they could try to turn it into a product. (I have a number of ideas, but not the time or motivation to work on them now.) The code above should be readable and if not, I can give you a walkthrough. Also, I have shared step-by-step instructions with @Johan Commelin that I'd be happy to share out with anyone.

#### Jason Rute (Jul 18 2020 at 22:12):

More about that tool can be found here: https://leanprover.zulipchat.com/#narrow/stream/144837-PR-reviews/topic/.232953.20submodule.2Esubtype/near/199815692

Last updated: May 18 2021 at 15:14 UTC