vscode extension

Stream: general

[Gabriel Ebner]

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]

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

[Daniel Fabian]

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]

There is a tactic extract_goal

[Johan Commelin]

It's not exactly what you describe

[Johan Commelin]

I usually write

/-
-/

and then paste the goal in it.

[Daniel Fabian]

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

[Johan Commelin]

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

[Johan Commelin]

And then remove the comments

[Daniel Fabian]

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

[Johan Commelin]

You can keybind it

[Johan Commelin]

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

[Daniel Fabian]

oh, what's the command called?

[Johan Commelin]

Something with freeze or sticky, I guess

[Alex J. Best]

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

[Johan Commelin]

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

[Bryan Gin-ge Chen]

Search for "toggle updating" in the keyboard shortcuts.

[Bryan Gin-ge Chen]

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]

there's sticky position

[Daniel Fabian]

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]

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]

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]

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

[Bryan Gin-ge Chen]

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]

I've found some in the default config of vscode

[Edward Ayers]

So far I've got:

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

[Kevin Buzzard]

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]

Would it be better to just not show anything?

[Kevin Buzzard]

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]

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

[Edward Ayers]

lean-0.15.15.vsix

[Kevin Buzzard]

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

[Kevin Buzzard]

ooh that fixed it

[Yakov Pechersky]

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

image.png

[Gabriel Ebner]

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]

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]

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]

It was actually @Jason Rute that wrote the secret tool

[Daniel Fabian]

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]

would that be easier?

[Bryan Gin-ge Chen]

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]

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

[Jason Rute]

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]

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]

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]

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