Zulip Chat Archive

Stream: general

Topic: vscode extension


view this post on Zulip 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.

view this post on Zulip Johan Commelin (May 14 2020 at 14:25):

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

view this post on Zulip 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.

view this post on Zulip Johan Commelin (May 14 2020 at 19:13):

There is a tactic extract_goal

view this post on Zulip Johan Commelin (May 14 2020 at 19:13):

It's not exactly what you describe

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

I usually write

/-
-/

and then paste the goal in it.

view this post on Zulip Daniel Fabian (May 14 2020 at 19:14):

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

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

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

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

And then remove the comments

view this post on Zulip 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.

view this post on Zulip Johan Commelin (May 14 2020 at 19:15):

You can keybind it

view this post on Zulip Johan Commelin (May 14 2020 at 19:15):

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

view this post on Zulip Daniel Fabian (May 14 2020 at 19:15):

oh, what's the command called?

view this post on Zulip Johan Commelin (May 14 2020 at 19:15):

Something with freeze or sticky, I guess

view this post on Zulip 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

view this post on Zulip Johan Commelin (May 14 2020 at 19:16):

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

view this post on Zulip Bryan Gin-ge Chen (May 14 2020 at 19:16):

Search for "toggle updating" in the keyboard shortcuts.

view this post on Zulip 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.

view this post on Zulip Daniel Fabian (May 14 2020 at 19:17):

there's sticky position

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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 .

view this post on Zulip 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.

view this post on Zulip Edward Ayers (Jun 19 2020 at 16:07):

I've found some in the default config of vscode

view this post on Zulip 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": ""
        }
    ],

view this post on Zulip 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.

view this post on Zulip Edward Ayers (Jun 19 2020 at 16:41):

Would it be better to just not show anything?

view this post on Zulip 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.

view this post on Zulip Edward Ayers (Jun 19 2020 at 16:44):

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

view this post on Zulip Edward Ayers (Jun 19 2020 at 16:50):

lean-0.15.15.vsix

view this post on Zulip 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.

view this post on Zulip Kevin Buzzard (Jun 19 2020 at 22:30):

ooh that fixed it

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip Johan Commelin (Jul 18 2020 at 17:04):

It was actually @Jason Rute that wrote the secret tool

view this post on Zulip 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.

view this post on Zulip Daniel Fabian (Jul 18 2020 at 19:16):

would that be easier?

view this post on Zulip 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.

view this post on Zulip 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...

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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